coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Miscellaneous fixes and improvements:	herbelin	2008-12-02
\| \| \| \| \| \| \| \| \| \| \|	- Fixed a virtual bug of unification (ever occurs if w_unify called with a non-empty context of rel's, which is a priori uncommon). - Fixed Notation.out test. - Add better coqide error message in case editor is called on an unnamed file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin	2008-11-07
\| \| \| \| \| \| \| \| \|	- Correction bug #1815 sur "coqide dir_inexistant/nom_fichier" - Tests oubliés de la révision 11438 (amélioration affichage coercions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11555 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des notations récursives:	herbelin	2008-10-22
\| \| \| \| \| \| \| \| \| \| \| \| \|	- Prise en compte des notations applicatives - Remplacement du codage des arguments liste des notations récursives sous forme de terme par une représentation directe (permet notamment de résoudre un problème de stack overflow de la fonction d'affichage) + Correction bug affichage Lemma dans ppvernac.ml + Divers util.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11489 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte réversibilité des notations de la forme "Notation Nil := ↵	herbelin	2007-05-10
\| \| \| \| \| \| \| \| \| \|	@nil". Ajout @ref au niveau constr pour allègement syntaxe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9819 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Exemple avec liaison des variables de filtrage du match	herbelin	2006-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9228 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Notations:	herbelin	2006-10-09
\| \| \| \| \| \| \| \| \| \| \| \|	- prise en compte des variables liées non liées par la notation (bug #1186), - test pour affichage des notations aussi sur les sous-ensembles des lieurs multiples (cf notation "#" dans output/Notations.v), - extension, correction et uniformisation de quelques fonctions sur les constr_expr et cases_pattern (avec incidences sur rawterm.ml, parsing et contrib/interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1179 (result of Notation.decompose_notation_key in wrong order	herbelin	2006-09-23
\| \| \| \| \| \| \|	leading to wrong/failing printing of notations such as "- 1" or "1 -"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9167 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction filtrage des notations impliquant un "match" : la présence	herbelin	2006-09-23
\| \| \| \| \| \| \| \| \| \|	des localisations empêchait toute unification des pattern de filtrage de réussir. - Ajout au passage d'unification des pattern modulo alpha. - Exemples dans Notations.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout test notation récursive	herbelin	2006-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7847 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test choix conflit afficheur de nombres selon la présence ou pas d'une coercion	herbelin	2006-01-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7798 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7701 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout suffixe 8 pour test en nouvelle syntaxe	herbelin	2004-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6446 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test lieurs dans Notation	herbelin	2004-11-17
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6309 85f007b7-540e-0410-9357-904b9bb8a0f7