aboutsummaryrefslogtreecommitdiff
path: root/syntax
AgeCommit message (Collapse)Author
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
2003-01-16Bugs affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3517 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-20Correction des priorités des TOMATCHherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3259 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-21Bug qui empêchait "0" d'être parenthèséherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3162 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-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@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29syntax/PPTactic.v passe au niveau MLherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2733 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
2002-05-27Ajout de Eval, Inst et Checkdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2711 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-11bad printing of Zeta reduction flags (was missing)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2465 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-01Ajout tactiques Rename et Pose; modifications pour Inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2449 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13Affichage NewInduction/NewDesctructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2294 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-06Affichage des '_' pour Introsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2276 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-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs ↵herbelin
'ClearBody H' et 'Assert H := c' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Mise en place d'un nouveau Destruct sur le modèle du nouvel Inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1874 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵herbelin
définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1808 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-04-24Reorganisation pour Ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1697 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Ajout de syntaxe pour Ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1677 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-13Reparation de l'affichage des THEN'sdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1588 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10Bug affichage LETPATTERNherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1567 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-27Interprétation des qualidargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1496 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23Les règles d'affichage ajoutés dans le commit précédent avait le même ↵herbelin
nom que la règle pour command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1484 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-22Règle de syntaxe pour CASTEDCOMMANDherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1478 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
2001-02-07Ajout du Match Contextdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1349 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-11-21Traitement du pretty-print des Redexpdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@911 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-10-03Renommage tactique Let en LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@644 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-11Bugsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@274 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@268 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:18:40 +0000