diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-09 13:27:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-09 13:27:03 +0000 |
| commit | ce7e64328553ac71f2630816cfb8baa930ea471e (patch) | |
| tree | e0669306e771ebc7e5b9a7712212c39047e44d2e /parsing | |
| parent | 1795451a803ffa38d9b5cbf38d93cc7df687c11f (diff) | |
Ajout de or-pattern pour le match-with v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
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 1103d41a2..61cff830d 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 7c573e07c..ded6e823f 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) |