coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	bug serieux efficacite de ltac	barras	2006-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8963 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Distinction explicite des parties paramètres et arguments dans le type	herbelin	2006-04-27
\| \| \| \| \| \| \| \|	des inductifs de la clause "in" du filtrage. - Débogage et extension du parseur xml (g_xml.ml4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8755 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin	2006-04-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	PCase dans le type pattern: le type pattern est utilisé essentiellement dans ltac, il est normalement obtenu sans typage, et ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à part car sans le type, il est impossible de savoir le nombre d'arguments du constructeur puisque par définition du "if", ceux-ci ne sont pas liants et ne laissent pas dans la syntaxe concrète (résolution au passage du bug #1070, dû à un filtrage incomplet dans le passage de pattern à rawconstr permettant l'affichage des pattern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	The type Pattern.constr_label was isomorphic to Libnames.global_reference.	sacerdot	2004-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6427 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
\| \| \| \| \| \| \| \| \| \| \|	the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 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
*	Substitution dans REvar et PEvar plutot que encodage via noeud application ↵	herbelin	2003-12-19
\| \| \| \| \| \|	pour eviter la confusion avec la (vraie) application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration afficheur de Cases pour les constr_pattern	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4110 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Preservation affichage des ?n en V7	herbelin	2003-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4060 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
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
\| \| \| \| \| \| \| \| \|	pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 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
*	Vraie substitutivite de autohints	coq	2002-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 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
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 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
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)	herbelin	2001-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1970 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	uniformisation avec constr des lieurs dans rawterm/pattern	herbelin	2001-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1377 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des noms longs dans les Hints et les Coercions, et ↵	herbelin	2001-01-24
\| \| \| \| \| \|	réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pattern sera mieux dans Pretyping; relâchement head_pattern_bound	herbelin	2000-12-26
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1219 85f007b7-540e-0410-9357-904b9bb8a0f7