coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin	2006-12-12
\| \| \| \| \| \| \| \| \| \|	cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml) + test régression bug #1041 + allègement syntaxe tactique evar + essai de ne pas faire dépendre les evars des variables anonymes afin de résoudre le bug #932 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9433 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout combinateurs option_fold_left et name_fold_map	herbelin	2006-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9225 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	name_app accessible a tous dans Nameops	herbelin	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5112 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fonctions utiles	herbelin	2003-09-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4460 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4115 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
\| \| \| \| \| \| \| \| \|	Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un traducteur de noms v7->v8	herbelin	2003-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petit netoyage dans lib	coq	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- 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
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation de Locate	barras	2001-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2247 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
*	GROS COMMIT:	barras	2001-11-05
	- 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