| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-08-27 | [numeral] [plugins] Switch from `Big_int` to ZArith. | Emilio Jesus Gallego Arias | |
| We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 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 |