coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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