coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-02	Remove the omega tactic and related options	Jim Fehrle

2019-05-23	Fixing typos - Part 3	JPR

2019-02-08	[test-suite] Improve test for async workers.	Emilio Jesus Gallego Arias

2019-02-08	[stm] Filter some more arguments that shouldn't be sent to workers.	Emilio Jesus Gallego Arias
	This fixes #9484 .
2018-12-18	Merge PR #9223: Fix universe restriction in delayed mode.	Pierre-Marie Pédrot

2018-12-17	Restrict body universes in delayed mode.	Gaëtan Gilbert

2018-12-17	Fix classification of Set Default Proof Mode.	Gaëtan Gilbert

2018-10-02	Update the -compat flags	Jason Gross
	Mostly via `dev/tools/update-compat.py --cur-version=8.9` We just remove test-suite/success/FunindExtraction_compat86.v because, except for the `Extraction iszero.` line at the bottom, it is a duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`). We also manually update a number of test-suite files to pre-emptively remove compatibility notations (which used to be compat 8.6, but are now compat 8.7).
2015-11-10	Updating test-suite after Bracketing Last Introduction Pattern set by	Hugo Herbelin
	default. Interestingly, there is an example where it makes the rest of the proof less natural. Goal forall x y:Z, ... intros [y\|p1[\|p2\|p2]\|p1[\|p2\|p2]]. where case analysis on y is not only in the 2nd and 3rd case, is not anymore easy to do. Still, I find the bracketing of intro-patterns a natural property, and its generalization in all situations a natural expectation for uniformity. So, what to do? The following is e.g. not as compact and "one-shot": intros [\|p1\|p1]; [intros y\|intros [\|p2\|p2] ..].
2015-07-31	Remove some outdated files and fix permissions.	Guillaume Melquiond

2013-10-03	Regression test suite for STM	gareuselesinge
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16840 85f007b7-540e-0410-9357-904b9bb8a0f7