diff options
| author | herbelin | 2007-04-10 16:36:36 +0000 |
|---|---|---|
| committer | herbelin | 2007-04-10 16:36:36 +0000 |
| commit | 8aa6ed2d10ddefb348f98684e691e25e4866b6ca (patch) | |
| tree | c286ad9f175e2c3088ea162da9df649134e15fa4 | |
| parent | 1fcdaed7fea598ff2724095c5476e8bdc04ef48a (diff) | |
Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5
tout en évitant que les .. soient dans constr)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9755 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 7 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 |
3 files changed, 10 insertions, 1 deletions
@@ -1,9 +1,16 @@ Changes from V8.1gamma to ... ============================= +Commands + - Added option Global to "Implicit Arguments" and "Arguments Scope" for section surviving. +Notations + +- Level "constr" moved from 9 to 5. User notations from levels 6 to 9 + may have to be put at levels below 5 to be used without parentheses. + Tactic Language - Second-order pattern-matching now working in Ltac "match" clauses diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index bdea94a048..f2316ec5e1 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -131,7 +131,7 @@ GEXTEND Gram [ [ c = operconstr LEVEL "200" -> c ] ] ; constr: - [ [ c = operconstr LEVEL "1" -> c ] ] + [ [ c = operconstr LEVEL "5" -> c ] ] ; operconstr: [ "200" RIGHTA @@ -160,6 +160,7 @@ GEXTEND Gram | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ] + | "5" LEFTA [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> CApp(loc,(Some (List.length args+1),CRef f),args@[c,None]) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index ecbc2ef6c0..8f23c0f30e 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -487,6 +487,7 @@ let default_levels = 90,Gramext.RightA; 10,Gramext.RightA; 9,Gramext.RightA; + 5,Gramext.LeftA; 1,Gramext.LeftA; 0,Gramext.RightA] |