Yannick Forster

I would say the expected behaviour is an error which says "constant Wrong.nat not found" or something similar. I'm particularly worried about the word "anomaly" occurring, we don't want people...

I agree with Gregory and Théo. Matthieu, would the translation require that stacked (binary) tApp in PCUIC get translated to one big Template Coq tApp (taking a term and a...

I think there's a problem, yes. If you start at `Ast.tApp u [v1, v2]` and you go to PCUIC you are `PCUIC.tApp (PCUIC.tApp u' v1') v2'` If you go back...

Oops, you're right. I had a wrong definition of `mkApps` in mind, this is indeed doing the unstacking properly, so everything is fine on this front.

Does the pretty printing work for those bytestrings as it works for strings? For debugging it's very important to be able to read the strings, rather than seeing their ASCII...

Would type soundness be needed for the correctness of extraction? Probably everything you would need is a definition of the OCAML light type system and a definition of evaluation on...

Ah, and as @mattam82 has mentioned before, OCaml light probably does not cover `Obj.magic`, which is inserted a lot by the extraction at points where the erased Coq terms have...

`#[missing=tactic]` would be similarly fine for me

There was a PR for Coq at some point (by Théo I think?) introducing a flag to make fixpoints unguarded. That would make a fixpoint combinator in the monad superfluos....

> I understand that these pimitives have been disabled again? Yes, the primitives have been disabled for the moment. The problem is that we don't have a good story how...