coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-12-02	Move unreleased changelog to new 8.11 section.	Théo Zimmermann

2019-11-28	[changelog] Add types to changelog entries.	Théo Zimmermann
	Types of changes are defined in the list defined by Keep a Changelog 1.0.0 (https://keepachangelog.com/en/1.0.0/): - Added - Changed - Deprecated - Fixed - Removed We exclude the type Security for now, even for soundness fixes, because the process of handling security vulnerabilities is different from anything we follow right now.
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