aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppconstr.ml
AgeCommit message (Collapse)Author
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
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
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
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
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-03Retour vieil afficheurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3727 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Retour nouvel afficheurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3709 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Rétablissement pr_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3527 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-07Retour printer ast pour V7.4herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3491 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Affinement affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3471 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3439 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Bugs diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3419 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Problèmes et améliorations affichage; Changement Simplherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3395 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-04Correction divers bugs d'affichage; explicitation du niveau de grammaire ↵herbelin
quand mentionn explicitement par l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3377 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-03bugs d'affichage (confusion key/scope dans les délimiteurs)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3366 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Re-déplacement du résultat de Grammar au niveau constr_exprherbelin
(globalisation uniquement des noms - sauf cases, fix, ..., pas d'implicites, pas d'interprétation des scopes - pas plus robuste qu'avant...). Diverses améliorations affichage et parsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3350 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-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵herbelin
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
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-09-27passage a ocaml 3.06herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3041 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-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2735 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 03:58:46 +0000