coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)	herbelin	2004-06-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage de l'opacité dans Print et About	herbelin	2004-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction oubli du cas pas d'arguments implicites du tout	herbelin	2004-03-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5414 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Expansion du type par nécessité dans le cas d'affichage d'implicites	herbelin	2004-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5398 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id ↵	herbelin	2004-01-29
\| \| \| \| \| \| \| \| \|	:= c" de "Notation "'id'" := c" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5264 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Print Implicit avec depliage du type	herbelin	2003-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4919 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Saut de ligne avant les infos non logiques de print_about	herbelin	2003-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4714 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de Locate	herbelin	2003-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4688 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ameliration affichage inductifs	herbelin	2003-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4615 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout fnl() dans About	herbelin	2003-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4599 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Inspect saute maintenant les marqueurs invisibles	herbelin	2003-10-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4535 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug about	herbelin	2003-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4492 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'About'	herbelin	2003-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des scopes d'arguments	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4376 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Impression sans ',' des constructeurs de meme type, pour v8	herbelin	2003-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4301 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des inductifs en v8	herbelin	2003-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4281 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tables logarithmiques pour les coercions + nettoyage	herbelin	2003-06-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
\| \| \| \| \| \| \| \|	(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : ↵	herbelin	2003-02-27
\| \| \| \| \| \|	color' pour les types énumérés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3716 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour satisfaire ProofGeneral	coq	2003-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deux p\'tits trucs ;)	coq	2003-01-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3614 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
*	possibilité de faire Print M avec M module ou modtype au lieu de Print ↵	letouzey	2002-12-13
\| \| \| \| \| \|	Module et Print Module Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3430 85f007b7-540e-0410-9357-904b9bb8a0f7
*	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey	2002-12-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3369 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin	2002-11-26
\| \| \| \| \| \| \| \|	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
*	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
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
\| \| \| \| \| \| \| \| \| \| \|	- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Des critères plus fins d'analyse des implicites automatiques; meilleur ↵	herbelin	2002-10-28
\| \| \| \| \| \|	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
*	Restriction sur la forme des Syntactic Definition et re-localisation en ↵	herbelin	2002-10-12
\| \| \| \| \| \|	fonction de l'endroit d'utilisation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3117 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Lazy manuelles dans le code	coq	2002-10-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Lazy experimentale temporaire...	coq	2002-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pretty-printing preliminaire des modules, commandes	coq	2002-08-19
\| \| \| \| \| \| \| \| \| \| \| \| \|	Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Strengthenning rules for modules + No modules in sections	coq	2002-08-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 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
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	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
*	Typo	herbelin	2002-04-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2647 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug affichage '++' au lieu de ';'	herbelin	2001-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2364 85f007b7-540e-0410-9357-904b9bb8a0f7
*	affichage correct du type des inductifs et constructeurs en presence	barras	2001-12-18
\| \| \| \| \| \| \|	de parametres git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2312 85f007b7-540e-0410-9357-904b9bb8a0f7
*	compat ocaml 3.03	filliatr	2001-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 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
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵	herbelin	2001-10-17
\| \| \| \| \| \|	sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 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
*	Marre des unrecognized objects	herbelin	2001-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2055 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration affichage de print_leaf_entry	herbelin	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2040 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Transparent	barras	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et ↵	herbelin	2001-09-19
\| \| \| \| \| \|	le «load» des Remark/Fact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1998 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rétablissement de Print Section	herbelin	2001-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1926 85f007b7-540e-0410-9357-904b9bb8a0f7