coq - The formal proof system

Age	Commit message (Collapse)	Author
2003-11-01	Renommage Topconstr.map_aconstr_with_binders_loc	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4764 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-11	Ajout option 'Local' à Infix et Notation	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3915 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31	Ajout d'un choix 'onlyparse'	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3822 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin
	Affinement de la gestion des niveaux de constr. Cablage en dur du parsing et de l'affichage des délimiteurs de scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14	Réforme de l'interprétation des termes :	herbelin
	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7