coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"	herbelin	2010-06-13
\| \| \| \| \| \| \| \| \| \| \| \|	by a regular error in v8.3. Example behaves better in trunk thanks to new proof engine. In fact, there are two distinct solutions to a unification problem: should "refine" commit to one of them or leave the problem open? For trunk, improved the unification error message by enforcing nf_evar (but at some time, nf_evar in error messages should move to himsg because it is costly when errors are used for backtracking). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13127 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which	herbelin	2010-04-07
\| \| \| \| \| \| \| \|	was actually failing for another reason than the reason originally filled in the bug tracker) and revealed a bug in the unification.v test file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12906 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 du format des messages d'erreur (commencent par une	herbelin	2008-07-17
\| \| \| \| \| \| \| \| \| \|	majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Temporarily disabling automatic test for bug 1338.v	notin	2008-06-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11041 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757	herbelin	2008-05-07
\| \| \| \| \| \| \|	+ un error qui devrait être un anomaly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10893 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug squashing day !	msozeau	2008-04-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Closed bugs 121, 1696, 1438, 1425, 1696, 1604, 1738, 1760, 1683 related to setoids. Add corresponding test files. - Add new modulo_zeta flag to control zeta during unification (e.g. not allowed for setoid_rewrite unification, but ok for almost everything else). - Various fixes in class_tactics with respect to evars and error messages. - Correct error message for NoOccurenceFound, distinguishing between a rewrite in the goal or an hypothesis. - Move notations for ==>, --> and ++> to level 90 as suggested by Russell O'Conor. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10813 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mises à jour bugs, CHANGES, code mort	herbelin	2008-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10801 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression	notin	2008-03-28
\| \| \| \| \| \| \| \|	d'un test non significatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10726 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Diverses petites modifs dans la test-suite:	notin	2008-03-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	test-suite/output/ZSyntax.out typo test-suite/bugs/closed/shouldsucceed/1776.v bug closed test-suite/success/extraction.v test-suite/success/extraction.v test-suite/bugs/closed/shouldsucceed/846.v backtrack sur le commit 10639 test-suite/bugs/closed/shouldsucceed/1322.v: petites modifications suite aux changement de setoid_replace test-suite/bugs/closed/shouldsucceed/1414.v: petites modifications suite aux changement dans Program git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10723 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de 2 tests	notin	2008-02-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fermeture du bug #1754	notin	2008-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10472 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un test pour le mode déclaratif + test pour le bug #1776	notin	2008-01-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10466 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1754	notin	2008-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajouts de quelques tests sur les bugs	notin	2007-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10400 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test pour le bug #1754	notin	2007-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10364 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans check + ajout de tests	notin	2007-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10134 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1634 + ajout de bugs dans la test-suite	notin	2007-08-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin	2007-08-16
\| \| \| \| \| \| \| \| \|	modification de interp_ltac_reference pour passer les ids utilisées dans le contexte d'appel d'une tactique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de la test suite pour intégrer des tests spécifiques aux	notin	2007-08-10
	bugs soumis sur Coq-bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10068 85f007b7-540e-0410-9357-904b9bb8a0f7