Yannick Forster

Thanks, that's very helpful! I'm mainly asking because we have very similar problems in the compilation chain MetaCoq -> [coq-library-undecidability](https://github.com/uds-psl/coq-library-undecidability/) -> [coq-library-complexity](https://github.com/uds-psl/coq-library-complexity). I'll have a look whether we can get...

I'd like to second this feature request :) We are basically done verifying extraction from Coq to Malfunction. Now to link with other OCaml libraries (e.g. with the OCaml implementation...

At least for our use case, this was covered by #35 now

I just synced all branches, I think we can move the default branch to be `coq-8.18` now. (Not `main`, because we don't want to give the impression that contributors are...

Is this PR still active or will it be subsumed by the upcoming proper integration of the FOL library?

If you want a hybrid printer printing both de Bruijn indices and names, you could change line 149 of `template-coq/theories/Pretty.v` to ``` | Some id => id ^ "(" ^...

Can we let the `patch` command fail if the patch is not applicable? If not, it might make sense to keep the orig file and fail if it is not...

Is that different to `|| exit`? But the idea seems to be the right one to enforce a failure on a failing patch

I think the problem is that you have MetaCoq installed as an opam package and want to build locally. That's what the ``` findlib: [WARNING] Package coq-metacoq-template-ocaml has multiple definitions...

Thanks a lot Karl for bringing this up! I'm in favour of changing the library to the weakest license possible: MIT. In the end, we want as many people as...