coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-12-04	[doc] coq_environment.txt	Enrico Tassi

2020-09-22	Merge PR #13049: [configure] Fix version checks for lablgtk and zarith	coqbot-app[bot]
	Reviewed-by: SkySkimmer Reviewed-by: vbgl Ack-by: Zimmi48 Ack-by: JasonGross
2020-09-17	[configure] Fix version checks for lablgtk and zarith	Emilio Jesus Gallego Arias
	Fixes #13041 #13047 Configure is quite messy, but we will improve it once we can link it with findlib and move to dune [that will actually allow to remove all ad-hoc calls to `ocamlfind` in favor of `findlib` code.
2020-09-17	[install] Rewording of primitive floats.	Emilio Jesus Gallego Arias
	As suggested in the PR review. Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
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-09-15	[zarith] [micromega] Bump to 1.10 and remove some hacks	Emilio Jesus Gallego Arias
	In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58
2020-09-14	[ci] [docker] Up testing to OCaml 4.11.1	Emilio Jesus Gallego Arias
	- `odoc` must be bumped to support 4.11
2020-09-10	Fix typos.	Théo Zimmermann
	Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-09-09	Update INSTALL.md	Matthieu Sozeau

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-05-14	Add advisories on OCaml setup to INSTALL.md.	Théo Zimmermann
	Closes #12232.
2020-03-29	[ci] [gitlab] Bump to edge to OCaml 4.10, add test-suite for OCaml 4.11	Emilio Jesus Gallego Arias

2020-03-18	[ci] [docker] Update to 4.09.1	Emilio Jesus Gallego Arias
	That release includes non trivial changes related C compilers, in particular due to `-fno-common` support.
2019-12-13	[doc] [INSTALL] split make-based install instructions to its own file.	Emilio Jesus Gallego Arias

2019-12-13	[doc] [INSTALL] Port INSTALL to markdown format.	Emilio Jesus Gallego Arias