diff options
| author | pboutill | 2011-07-22 13:26:27 +0000 |
|---|---|---|
| committer | pboutill | 2011-07-22 13:26:27 +0000 |
| commit | 2145319442699bb3a2ab0158ea702fa2558a5150 (patch) | |
| tree | 9003e71012236a26a7aa8ea583f92ab8ad93de45 /parsing | |
| parent | 3bc1612a8b3a7c5ab52c3cd68cc1670b916438c0 (diff) | |
Add a syntax entry for fully applied constructor pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14292 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 7 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 3 |
2 files changed, 8 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index fa0e2fe52a..5d5f6e4d45 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -320,14 +320,17 @@ GEXTEND Gram [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ] | "99" RIGHTA [ ] | "10" LEFTA + [ p = pattern; "as"; id = ident -> + CPatAlias (loc, p, id) ] + | "9" RIGHTA [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Util.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Constructor expected.")) - | p = pattern; "as"; id = ident -> - CPatAlias (loc, p, id) ] + |"@"; r = Prim.reference; lp = LIST1 NEXT -> + CPatCstrExpl (loc, r, lp) ] | "1" LEFTA [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ] | "0" diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index c1466f9a02..811f170dc8 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -177,6 +177,9 @@ let rec pr_patt sep inh p = | CPatCstr (_,c,[]) -> pr_reference c, latom | CPatCstr (_,c,args) -> pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + | CPatCstrExpl (_,c,args) -> + assert (args <> []); + str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp | CPatAtom (_,None) -> str "_", latom | CPatAtom (_,Some r) -> pr_reference r, latom | CPatOr (_,pl) -> |