coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-25	[ocamlformat] Use doc-comments=before style.	Emilio Jesus Gallego Arias
	IMHO it is a bit more logical, WDYT?
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-12-13	[micromega] Enable ocamlformat.	Emilio Jesus Gallego Arias

2019-09-16	Re-implementation of zify	Frédéric Besson
	The logic is implemented in OCaml. By induction over the terms, guided by registered Coq terms in ZifyInst.v, it generates a rewriting lemma. The rewriting is only performed if there is some progress. If the rewriting fails (due to dependencies), a novel hypothesis is generated. This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848 ans fixes #10755. The zify plugin is placed in the micromega directory. (Though the reason is unclear, having it in a separate directory is bad for efficiency.) efficiency impact. There are also a few improvements of lia/lra that are piggybacked. - more aggressive pruning of useless hypotheses - slightly optimised conjunctive normal form - applies exfalso if conclusion is not in Prop - removal of Timeout in test-suite
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-05-23	Fixing typos - Part 2	JPR

2018-10-16	[micromega] remove dead code	Vincent Laporte

2018-06-07	Micromega clean-up	Maxime Dénès
	We add .mli files, removed dead code and use standard combinators instead of redefined ad-hoc ones in a few places. A lot of cleaning still has to be done on this code: documenting the interfaces, resolving the many abstraction leaks. I suspect there is still a lot of code duplication.