Rodolphe Lepigre

@fblanqui: if the object is defined with `theorem`, then the proof term is not recorded after the `qed` (see [here](https://github.com/Deducteam/lambdapi/blob/c01b734c6ceb94d7b83dc06540cb33c062ab5ca5/src/handle.ml#L225-L228)). Obviously, partial proofs are stored until the proof term is...

Couldn't you use local let-definitions to embed the intermediate result in the proof of the final results? This would probably not change much the size of the initial file if...

I am not surprised at all that Lambdapi yields bigger object files (this has always been the case). This is due to the fact that they contain closures (Bindlib binders)....

Thanks for the report! That's a weird issue! I investigated a bit and I was unable to fix the problem quickly. In fact, I managed to make things work (seemingly)...

The HTML driver (although it exists) never properly worked due to font problems, but you can still generate documents for the we browser using the SVG driver. It generates HTML...

At some point yes, but I personally don't have time to take care of that right now.

Do you mean that the environment variable INSTALL_UNICODELIB_DIR (set by configure.ml) does not always coincides with the directory in which ocamlfind actually installs unicodelib? What kind of value do you...

I agree. It would probably be best if the `get_config` function (in `configure.ml`) guessed the configuration from `ocamlfind` instead of `opam` (and maybe check that both configurations agree).

Hi! Thanks for trying! That's really weird, I can't reproduce. Are you running Linux? Have you installed the required libraries by hand? With Opam?

OK, I see. I can't see any problem with that (but yeah, you should install opam 2 since the central repository has moved to opam 2 format). Installing `earley` by...