Matthieu Sozeau
Matthieu Sozeau
We still use the Export in erasure apparently :)
Still not exactly right, maybe because we merged something else in the meantime ;)
Shall we fix this @yforster ?
Sure! Do you think the current `.opam` files will work easily? I wonder what's the most efficient way to do that.
About the changes to erasure that would be necessary to target ocamllight: certainly quite a few Obj.magics would be needed for dependently-typed code. About linking to CertiCoq, we discussed a...
That sounds slightly dangerous, how about `#[missing=tactic]` or something similar? @TheoWinterhalter do you have this use case as well?
Ah yes, it's missing a name clash test or a proper shadowing discipline here.
Your example is slightly different @MevenBertrand , the ones of @jakobbotsch are fixed (with an explicit error from Equations). In your case the definition should go through but there is...
Indeed, I’d rather avoid the complications but it’s not so hard to implement
This should be mentionned in the manual/readme