coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Prise en compte noms longs dans SuperAuto	herbelin	2001-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1391 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du Let pour le langage de tactiques	delahaye	2000-12-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout ident_or_constrarg pour NewInduction	herbelin	2000-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1167 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewrite	herbelin	2000-12-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1133 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Notion de 'clause_pattern' pour désigner un ensemble d'occurrences dans le ↵	herbelin	2000-12-06
\| \| \| \| \| \|	but et ses hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1065 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restruration autour de qualidarg	herbelin	2000-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@962 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout diverses entrées pour les noms qualifiés	herbelin	2000-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@889 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place de parseurs avec globalisation pas seulement dans les ↵	herbelin	2000-10-18
\| \| \| \| \| \|	quotations, pour utilisation par les règles de syntaxe et grammaire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@718 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout castedopenconstrarg	herbelin	2000-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@643 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pattern matching de sous-termes + exceptions dans le lexer	delahaye	2000-08-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@578 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de piquants dans les actions des grammaires; nom de la grammaire pris ↵	herbelin	2000-07-28
\| \| \| \| \| \|	comme parseur par defaut; le type List devient AstList git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@575 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du langage de tactiques	delahaye	2000-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fin du changement comarg -> constrarg	herbelin	2000-01-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@283 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bête renommage	herbelin	2000-01-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@279 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage des fichiers de parsing	herbelin	2000-01-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@277 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration printer et parser	herbelin	2000-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@263 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modules Ast et Pcoq	filliatr	1999-09-08
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@53 85f007b7-540e-0410-9357-904b9bb8a0f7