From ce7e64328553ac71f2630816cfb8baa930ea471e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Sep 2004 13:27:03 +0000
Subject: 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
---
 parsing/g_constrnew.ml4 | 6 ++++--
 parsing/ppconstr.ml     | 4 ++++
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'parsing')

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)
-- 
cgit v1.2.3