I think if we wanted to implement deprecated for gallina terms we would do it when tackling CEP 42 https://github.com/coq/ceps/pull/42
I had a look a while back, and extending all the warnings etc. to gallina terms will take some work
I don't think this has much to do with that CEP though.
it's just a matter of adding a warning in the pretyper, this should cover 90% of the use-cases
(to whomever wants to implement that: just tweak Pretyping.pretype_ref
)
actually, maybe the intern phase would be a better place otherwise this will get spammy with tactics using internally glob constrs
What would happen if you deprecated an instance? Would typeclass search spam it every time it was checked?
no, this is already resolved by then
you'd see it for uconstr:() and the like
if you put the warning in intern it should only impact uses directly in the code
yep, this looks like the desired behaviour
(there will be a few misses like e.g. commands that take a globref as argument but this can be done in a second time)
12 messages were moved here from #Coq users > Compilation error in coq-json with coq-dev GitHub action by Ali Caglayan.
constrintern?
somewhere around Constrintern.intern_reference
Cool I'll see what I can do later
or intern_qualid
rather
You could even put it in vernac
not?
But if you deprecate an expression how will you throw a warning without interpreting it?
ah never mind
indeed the registration should go there
of course you need to put in the name resolution in interp
I'm a bit tired I guess
Last updated: Jun 08 2023 at 04:01 UTC