aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Collapse)AuthorAge
* Protection table des locations lors de Load (pour coqdoc)Gravatar herbelin2004-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5237 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5149 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug: faut brancher la sortie des tactiques sur stdout pendant traductionGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place traduction des tactiques apres evaluation pour permettre des ↵Gravatar herbelin2003-11-09
| | | | | | changements semantiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4839 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug traduction de auto.(simpl). en auto.simpl.Gravatar barras2003-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4676 85f007b7-540e-0410-9357-904b9bb8a0f7
* oups! ca compile maintenantGravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4656 85f007b7-540e-0410-9357-904b9bb8a0f7
* translator avoids printing a . followed by a ( by inserting a spaceGravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4655 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
* pr_vernac est paresseux; States.unfreeze seulement après que msgnl aitGravatar herbelin2003-10-03
| | | | | | | dégelé pr_vernac; hack pour "Import nat_scope" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4524 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction aussi si -translate et -load-vernac-sourceGravatar herbelin2003-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4471 85f007b7-540e-0410-9357-904b9bb8a0f7
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
| | | | | | | extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plutôt que de faire "Load" silencieusement, en profiter pour traduireGravatar herbelin2003-09-18
| | | | | | | le fichier chargé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour cacher le contenu de Load au traducteurGravatar herbelin2003-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4403 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debranchement du traducteur pour Load !Gravatar herbelin2003-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4347 85f007b7-540e-0410-9357-904b9bb8a0f7
* Freeze mal placeGravatar herbelin2003-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4293 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug et amliorations diversesGravatar herbelin2003-08-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4263 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout systématique de Proof dans la traductionGravatar herbelin2003-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4202 85f007b7-540e-0410-9357-904b9bb8a0f7
* Possibilité de syntaxe conjointement à la définition des inductifs et des ↵Gravatar herbelin2003-05-21
| | | | | | 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
* Affichage commentairesGravatar herbelin2003-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des produits de même type; parenthèses autour des x:=c et ↵Gravatar herbelin2003-04-29
| | | | | | n:=c dans les 'with bindings'; mise en place d'un 2ème traducteur à l'essai (activable avec -ftranslate2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug fermeture de stdoutGravatar herbelin2003-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Formattage affichageGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mécanisme plus simple et efficace pour traduire les implicitesGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs synchronisation pour gestion traduction des implicitesGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-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 ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Recuperation des outputs de l'interpretation des commandes vernac et des ↵Gravatar desmettr2003-02-28
| | | | | | erreurs pour le traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Undo dans Coq IDEGravatar filliatr2003-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du traducteurGravatar desmettr2003-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement du test 'il reste des preuves en cours'Gravatar filliatr2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3544 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout options -v7 et -v8, et commandes V7only et V8onlyGravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3407 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-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\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Error_in_file redondant et inappropriéGravatar herbelin2002-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-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
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
* compat ocaml 3.03Gravatar filliatr2001-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
* - condition de garde (suite)Gravatar barras2001-12-10
| | | | | | | - commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
* corrections mineures suite au commit de restructuration du noyauGravatar barras2001-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-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 ↵Gravatar herbelin2001-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
* Le fichier .vo etait ecrit dans un mauvais repertoire si ce dernier etait ↵Gravatar herbelin2001-09-26
| | | | | | trouve dans le path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option et d'une fonction compile pour fabriquer les .voGravatar herbelin2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1984 85f007b7-540e-0410-9357-904b9bb8a0f7
* nettoyage d'entrees de grammaires inutilesGravatar courant2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1563 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Import module force l'ouverture du module même s'il était déjà ouvert ↵Gravatar herbelin2000-12-20
| | | | | | afin de pouvoir re-rendre visible des noms ayant été cachés depuis l'ouverture du module; renommage de open_module en import_module avec cette nouvelle spéc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une capsule pour save_module_to dans DischargeGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@854 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouveau load pathGravatar filliatr2000-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
| | | | | | | Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@590 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 11:54:20 +0000