aboutsummaryrefslogtreecommitdiff
path: root/toplevel/command.ml
AgeCommit message (Collapse)Author
2004-01-13Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables ↵herbelin
a b:A' et 'Variables (a:A) (b:A)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5198 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-02meilleure presentation des commentaires du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4710 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Changement 'as notation' en 'where notation'; Plus d'uniformite dans la ↵herbelin
gestion des implicites d'inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4629 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Admitted rendu independant de Conjecture: plus pratique en mode interactifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4624 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Bug introduit dans start_proof par le commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4621 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Protection contre les noms de lemmes existant dejaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4607 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Prise en compte des paramètres implicites d'inductifs pour la globalisation ↵herbelin
des types de constructeur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4548 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé ↵herbelin
incomplètement prouvé comme axiome git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-16(Re-)branchement sur les noms reserves pour les args d'inductif (dont ↵herbelin
Record); args scope dans Declare git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4401 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Déplacement de Declare et déclarations des scopes d'argument dans Declareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4362 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ↵herbelin
| S (n:nat)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4282 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Mise en place structure pour des 'arguments scope' dirigés par une classeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4118 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ↵herbelin
points-fixes; prise en compte par le traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4042 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
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
2003-04-17Ajout "at next level" dans Notationherbelin
Mise en place structure pour définir un objet en même temps que sa notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3916 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
(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
2003-03-31Ajout d'un choix 'onlyparse'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3822 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Implicit Variables Type dans les inductiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3808 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19Petit netoyage dans libcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Prise en compte des scopes traversés dans les notationsherbelin
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
2002-12-09Code mort ?herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3391 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Réaffichage des Syntactic Definition (printer constr_expr).herbelin
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
2002-11-15Passage à une représentation des fixpoints plus primitive dans constr_expr ↵herbelin
(càd avec indices) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3245 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Ré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-11-06Un Local construit par preuve hors section doit être considéré globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3216 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- 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
2002-10-23Clarification changements autour de Remark/Fact/Localherbelin
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
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3045 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3043 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-17Suppression automatique du corps des définitions locales opaques dansherbelin
les contextes de preuves git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2972 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pourherbelin
les définitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2852 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Intgration uniforme de coercions dans les dclarations (Variable and co) et ↵herbelin
retouche des Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2747 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau 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
2002-02-15petits changements cosmetiques sur les tactiquesbarras
+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Prise en compte des '?' aussi dans le type des définitionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2228 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Mise en place d'une méthode directe pour indiquer le type des déclarations ↵herbelin
à toplevel plutôt que de passer par mkCast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS 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-26Vérification précoce qu'un lemme n'existe pas déjàherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2142 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et ↵herbelin
le «load» des Remark/Fact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1998 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14Transformation de Remark/Fact en constantes non visibles sans qualificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1969 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-21 07:02:49 +0000