I'm creating a new topic for naming/lemmas research, is that ok ?
(deleted)
yes always create new topics for new stuff, it's the recommanded usage!
What do you want to say though?
I was looking for the new name of flim_trans
and for near_eq_cvg
. Found them now :)
Indeed, they were part of the last big renaming
That was PR199 right ? Is the renaming described precisely somewhere, with flim -> cvg ?
I am struggling to adapt my fork of holomorphy.v, which dates back to february.
I don't think there is much more than the PR and its conversation
but I don't understand: I think I did it on the branch cauchy_etoile
mkerjean said:
That was PR199 right ? Is the renaming described precisely somewhere, with flim -> cvg ?
affeldt-aist said:
I don't think there is much more than the PR and its conversation
yes there is
I provide a sed script for the migration
If you have trouble using it, I can do the migration for you if you first rebase yourself on top of the commit math-comp/analysis#283b4330aa4327640c6e6a499c861ebc714ddd18
I don't think there is much more than the PR and its conversation
yes there is
Indeed, my mistake, I forgot: the file is pr193.sed
in the directory etc
.
Last updated: Oct 13 2024 at 01:02 UTC