coq - The formal proof system

Age	Commit message (Collapse)	Author
2003-11-15	Ajout Print Implicit avec depliage du type	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4919 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07	Inspect saute maintenant les marqueurs invisibles	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4535 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26	Ajout 'About'	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4484 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
2002-10-28	Des critères plus fins d'analyse des implicites automatiques; meilleur ↵	herbelin
	affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3185 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02	Modules dans COQ\!\!\!\!	coq
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin
	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05	GROS COMMIT:	barras
	- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-28	Pretty -> Prettyp	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7