diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constrnew.ml4 | 6 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 4 |
2 files changed, 8 insertions, 2 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index 1103d41a2e..61cff830d0 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -285,8 +285,10 @@ GEXTEND Gram [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ] ; pattern: - [ "10" LEFTA - [ p = pattern ; lp = LIST1 (pattern LEVEL "0") -> + [ "100" LEFTA + [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ] + | "10" LEFTA + [ p = pattern; lp = LIST1 (pattern LEVEL "0") -> (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Util.user_err_loc diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 7c573e07cc..ded6e823f9 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -219,6 +219,10 @@ let rec pr_cases_pattern _inh = function prlist_with_sep spc (pr_cases_pattern _inh) pl ++ str ")") | CPatAtom (_,Some c) -> pr_reference c | CPatAtom (_,None) -> str "_" + | CPatOr (_,pl) -> + str "(" ++ + hov 0 (prlist_with_sep pr_bar (pr_cases_pattern _inh) pl) ++ + str ")" | CPatNotation (_,"( _ )",[p]) -> str"("++ pr_cases_pattern _inh p ++ str")" | CPatNotation (_,s,env) -> fst (pr_patnotation pr_cases_pattern s env) |