coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option Local à Hint, Hints et HintDestruct	herbelin	2003-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de code dans command; MAJ DebugOn	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4119 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout V8Notation	herbelin	2003-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4061 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
*	Prise en compte des syntaxes v8 dans Uninterpreted Notation	herbelin	2003-04-29
\| \| \| \| \| \| \| \| \|	Suite mise en place infrastructure pour déclaration de syntaxe simultanée à la déclaration d'inductifs Table séparée pour les précédences de notations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3983 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option 'Local' à Infix et Notation	herbelin	2003-04-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3916 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction Show Implicits	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3891 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargs	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3888 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
*	Options d'affichage maintenant dans Constrextern	herbelin	2003-04-07
\| \| \| \| \| \| \|	Ajout "Set/Unset Printing Implicits" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3846 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
*	Ajout de Set Print Width	gregoire	2003-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3790 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
*	Debugger plus informatif	delahaye	2003-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du traducteur	desmettr	2003-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 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
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵	herbelin	2003-01-19
\| \| \| \| \| \|	la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵	herbelin	2003-01-15
\| \| \| \| \| \|	une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export M + Module M <: SIG	coq	2003-01-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	SearchAbout	filliatr	2003-01-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3489 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des scopes traversés dans les notations	herbelin	2002-12-15
\| \| \| \| \| \| \| \|	Traitement spécial pour le scope type_scope à l'internalisation Ajout "Locate Notation" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3441 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du vernac Proof with	gregoire	2002-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin	2002-12-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3418 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction divers bugs d'affichage; explicitation du niveau de grammaire ↵	herbelin	2002-12-04
\| \| \| \| \| \|	quand mentionn explicitement par l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3378 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification Require From	mohring	2002-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3376 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout des options "Set Contextual Implicits" et "Set Strict Implicits	herbelin	2002-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3351 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Raffinement syntaxe Infix	herbelin	2002-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3344 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵	herbelin	2002-11-24
\| \| \| \| \| \|	améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 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
*	Clarification changements autour de Remark/Fact/Local	herbelin	2002-10-23
\| \| \| \| \| \| \|	Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3180 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Redéplacement de + (sum) et * (prod) au niveau de + et * de ↵	herbelin	2002-10-22
\| \| \| \| \| \|	l'arithmétique; ajout d'une option 'level' pour Notation; utilisation de Notation pour sumor et sumbool git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3173 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une	herbelin	2002-10-14
\| \| \| \| \| \| \|	référence donnée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3133 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ↵	herbelin	2002-10-13
\| \| \| \| \| \|	hack temporaire autour du printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3120 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Encore quelques rangements dans Nametab + petits trucs	coq	2002-09-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3039 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nametab data structure reorganisation	coq	2002-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3030 85f007b7-540e-0410-9357-904b9bb8a0f7
*	La notation with dependante + affichage dependante de moduels corrige	coq	2002-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 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
*	Petites corrections ici et la	coq	2002-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 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
*	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin	2002-07-11
\| \| \| \| \| \| \|	les définitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de FNL ou utilisation de msgnl	herbelin	2002-06-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intgration uniforme de coercions dans les dclarations (Variable and co) et ↵	herbelin	2002-06-03
\| \| \| \| \| \|	retouche des Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2747 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
*	Plusieurs arguments autorisés pour Require et Read Module	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + ↵	herbelin	2001-12-16
\| \| \| \| \| \|	suppression des @Coercion, @Local et @Local Coercion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2299 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
*	- condition de garde (suite)	barras	2001-12-10
\| \| \| \| \| \| \|	- commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7