Pierre-Marie Pédrot
Pierre-Marie Pédrot
@JasonGross do you really want to keep fcl backwards compatible up to very old versions of Coq? I though that the only reason we kept it in the CI was...
Info_autorewrite is not exactly the same thing as the warning for non-imported hints, though. You'd have to perform some post-processing on the output of the first to get the second....
Any assignee? Not sure if I'm the most indicated one for this.
@SkySkimmer Currently you can't remove private constants from the environment because you need them in the nametab. There is the infamous `abstract foo using bar` variant that allows giving a...
FTR I've been advocating for replacing all primitive Prop-living axioms by an SProp variant, so that we recover canonicity in a systematic way.
@vblot this would need adding new primitive reductions to the various machines, including potential opcodes to the VM.
It's fragile and ad-hoc, and increases the TCB.
1. Decidable types have UIP. 2. What @silene means is that there is only one proof of equality in the empty context.
OK, I am being confusing, sorry about that. There are two meanings for UIP over a type `A`, - first the fact that given any equality type (in Prop, in...
Actually, we don't have to introduce an opcode for this. We could write an untyped program in the VM using the low-level equality and returning refl when the two arguments...