coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
\| \| \| \| \| \| \| \| \| \|	The manual has long stated that these forms are deprecated. We add a warning for them, as indeed `Add Morphism` is an "proof evil" [] command, and we may want to remove it in the future. We've also fixed the stdlib not to emit the warning. [] https://ncatlab.org/nlab/show/principle+of+equivalence
*	An example which failed in 8.5 and that d670c6b6 fixes.	Hugo Herbelin	2016-04-07
\| \| \| \|	Thanks to Matthieu for the example.
*	Fixing an incorrect use of prod_appvect on a term which was not a	Hugo Herbelin	2016-03-28
\| \| \| \| \| \| \| \| \| \|	product in setoid_rewrite. Before commit e8c47b652, it was raising an error which has been turned to an anomaly. This impacted Compcert where the former error was (apparently) caught so that setoid_rewrite was returning back to ordinary rewrite.
*	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
*	Fix [setoid_rewrite] forgetting some evars that are produced when ↵	msozeau	2013-06-10
\| \| \| \| \| \| \| \| \|	typechecking a lemma to apply, fixes test-suite test. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16569 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
\| \| \| \| \| \| \|	Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix inductive_template building ill-typed evars, and update test-suite scripts	msozeau	2011-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13909 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix test-suite script.	msozeau	2011-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13846 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correct handling of existential variables when multiple different	msozeau	2011-02-08
\| \| \| \| \| \| \| \| \|	instances of the lemma are rewritten at once. Cleanup dead code and put the problematic cases in the test-suite. Also fix some test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13813 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation of some error messages + added test on setoid rewrite.	herbelin	2009-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11765 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix setoid tests, use red for a Setoid_Theory lemma, and Parametric	msozeau	2008-04-14
\| \| \| \| \| \| \|	Relation for function spaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10786 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New implementation of Add Relation as a DefaultRelation instance	msozeau	2008-03-08
\| \| \| \| \| \| \| \|	declaration. Really fix bug#1704, correct order of condition subgoals even in setoid_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	implementation. Mostly syntax changes when declaring parametric relations, but also some declarations were relying on "default" relations on some carrier. Added a new DefaultRelation type class that allows to do that, falling back to the last declared Equivalence relation by default. This will be bound to Add Relation in the next commit. Also, move the "left" and "right" notations in Program.Utils to "in_left" and "in_right" to avoid clashes with existing scripts. Minor change to record to allow choosing the name of the argument for the record in projections to avoid possible incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test de non-régression pour commit 9673	herbelin	2007-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9709 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* setoid_test.v removed and added again in new syntax	sacerdot	2004-09-03
\| \| \| \| \| \| \|	* setoid_test.v8 ported to the new implementation of setoid_*. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6051 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout d'un fichier test pour setoides	clrenard	2001-09-25
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2069 85f007b7-540e-0410-9357-904b9bb8a0f7