| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-09-17 | [build] Don't link `num` anymore in Coq | Emilio Jesus Gallego Arias | |
| After #8743 we don't depend on `num` anymore in the codebase; thus we drop the dependency. This could create problems for plugins relying on this implicit linking. | |||
| 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 |