Matthieu Sozeau

functions which shouldn't be generalized blindly. In general the strategy for generalizing the arguments of the function for functional elimination seems suboptimal. It might try to generalize arguments that are...

For coq/coq#6285 (on top of #13952) This introduces an extension of Hint Extern, that is only available through `typeclasses eauto` in Coq. There is some continuation passing magic here so...

Don't merge yet, depending on Coq PR coq/coq#13952

ML code compatibility for Coq PR # 6285

5

Do not merge yet. Follows coq/coq#6285

These two new commands allow not only to compile to C but to build executables and run them from Coq directly, for faster testing. The new `CertiCoq Register [] Include...

Pointed out by Éric Tanter

Move coq-metacoq-template (and dependencies) to the "full" level

2

We can keep the other packages in extended, they change much more often.

… test to gc_stack.c

Our opam file will require clang for now (see PR #62 ) , as gcc is usually too slow and we barely tested CompCert's ccomp AFAIK. We should add a...