diff options
| author | herbelin | 2006-07-12 10:06:40 +0000 |
|---|---|---|
| committer | herbelin | 2006-07-12 10:06:40 +0000 |
| commit | 21f062a20d5170ba88c76a6c96111b3c70d0f76a (patch) | |
| tree | 042c5d9352832a98f93824f69b6cc5b194cb94ab | |
| parent | 2c18a485ee162c63046b9d087bf74e6b3c4f7a06 (diff) | |
Correction incohérence parsing de %delim dans les motifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9043 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_constr.ml4 | 8 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 |
2 files changed, 5 insertions, 4 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 935f6edcfc..641abe2f71 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -283,16 +283,16 @@ GEXTEND Gram [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ] | "99" RIGHTA [ ] | "10" LEFTA - [ p = pattern; lp = LIST1 (pattern LEVEL "0") -> + [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Util.user_err_loc (cases_pattern_loc p, "compound_pattern", Pp.str "Constructor expected")) | p = pattern; "as"; id = ident -> - CPatAlias (loc, p, id) - | c = pattern; "%"; key=IDENT -> - CPatDelimiters (loc,key,c) ] + CPatAlias (loc, p, id) ] + | "1" LEFTA + [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ] | "0" [ r = Prim.reference -> CPatAtom (loc,Some r) | "_" -> CPatAtom (loc,None) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index abe0d84265..92c68ff94e 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -488,6 +488,7 @@ let default_pattern_levels = 100,Gramext.RightA; 99,Gramext.RightA; 10,Gramext.LeftA; + 1,Gramext.LeftA; 0,Gramext.RightA] let level_stack = |