| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-04-11 | [dune] [stdlib] Build the standard library natively with Dune. | Emilio Jesus Gallego Arias | |
| This completes a pure Dune bootstrap of Coq. There is still the question if we should modify `coqdep` so it does output a dependency on `Init.Prelude.vo` in certain cases. TODO: We still double-add `theories` and `plugins` [in coqinit and in Dune], this should be easy to clean up. Setting `libs_init_load_path` does give a correct build indeed; however we still must call this for compatibility? | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |