aboutsummaryrefslogtreecommitdiff
path: root/syntax/PPConstr.v
AgeCommit message (Collapse)Author
2005-12-26Suppression des fichiers .v en ancienne syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7733 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Preservation affichage des ?n en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4060 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Affichage METAherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4035 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-27Affichage des Fix contenant des Let dans leur context (ce que la tactique ↵herbelin
Fix permet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3959 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-26Ajout de Set Print Widthgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3790 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-20Introduction d'un constructeur ARROW; rétablissement priorités desherbelin
arguments de APPTAIL (autre méthode dans g_constr.ml4 pour gérer le conflit entre "(f 3+4)" et "(f 3!x)") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3260 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-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur ↵herbelin
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
2002-10-14Parenthèses forcées autour des arguments d'une application pour parserherbelin
les expressions comme "(f (x+1))" (anticipation sur nouvelle syntaxe) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3135 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Ajout EVALherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2723 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]bherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2170 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
n'etaient pas affiches correctement lors du Save si on les avait donne en argument de tactique. Avec Bruno, nous avons simplifie l'ast en remplacant les MLCASE NOREC et autres CASE NOREC par des choses plus simples. Il y a maintenant un noeud LET, un IF, un CASE et un MATCH qui sont a peu pres semblables mais qui permettent de se souvenir quoi afficher. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1781 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Facilites pour le debogguage des univers.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Affichage des QUALIDherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@934 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Parsing des motifs de Syntax avec la grammaire associée à l'univers de la ↵herbelin
déclaration (constr, tactic ou vernac) au lieu de ast (comme cela a été fait pour Grammar) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@721 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Niveau d'associativité du letherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@688 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Code mort (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@663 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@662 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Bugs parenthèsesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@607 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
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@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-23Réparation bug d'affichage et affichage des instanciations par des {...}herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@472 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Déplacement du type reference dans Termherbelin
Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@383 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-20Affichage des <> pour débugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@330 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Renommage command en constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@262 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:32:22 +0000