Prise en compte des délimiteurs dans les motifs de Cases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3164 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 16 insertions, 7 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 40c2162daa..e1efe655a7 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -192,7 +192,7 @@ let may_allow_variable loc allow_var l =
         str "This reference does not denote a constructor: " ++
         str (string_of_qualid (interp_qualid l)))
 
-let maybe_constructor allow_var env = function
+let maybe_constructor allow_var = function
   | Node(loc,"QUALID",l) ->
       let qid = interp_qualid l in
       (try match extended_locate qid with
@@ -352,16 +352,16 @@ let message_redundant_alias (s1,s2) =
   warning ("Alias variable "^(string_of_id s1)
 	   ^" is merged with "^(string_of_id s2))
 
-let rec ast_to_pattern (_,_,scopes as env) aliases = function
+let rec ast_to_pattern scopes aliases = function
   | Node(_,"PATTAS",[Nvar (loc,s); p]) ->
       let aliases' = merge_aliases aliases (name_of_nvar s) in
-      ast_to_pattern env aliases' p
+      ast_to_pattern scopes aliases' p
 
   | Node(_,"PATTCONSTRUCT", head::((_::_) as pl)) ->
-      (match maybe_constructor false env head with
+      (match maybe_constructor false head with
 	 | ConstrPat (loc,c) ->
 	     let (idsl,pl') =
-	       List.split (List.map (ast_to_pattern env ([],[])) pl) in
+	       List.split (List.map (ast_to_pattern scopes ([],[])) pl) in
 	     (aliases::(List.flatten idsl),
 	      PatCstr (loc,c,pl',alias_of aliases))
 	 | VarPat (loc,s) ->
@@ -379,8 +379,11 @@ let rec ast_to_pattern (_,_,scopes as env) aliases = function
       Symbols.interp_numeral_as_pattern loc (Bignat.NEG (Bignat.of_string n))
 	(alias_of aliases) scopes)
 
+  | Node(_,"PATTDELIMITERS", [Str(_,sc);e]) ->
+      ast_to_pattern (sc::scopes) aliases e
+
   | ast ->
-      (match maybe_constructor true env ast with
+      (match maybe_constructor true ast with
 	 | ConstrPat (loc,c) -> ([aliases], PatCstr (loc,c,[],alias_of aliases))
 	 | VarPat (loc,s) ->
 	     let aliases = merge_aliases aliases (name_of_nvar s) in
@@ -577,7 +580,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
   and ast_to_eqn n (ids,impls,scopes as env) = function
     | Node(loc,"EQN",rhs::lhs) ->
 	let (idsl_substl_list,pl) =
-	  List.split (List.map (ast_to_pattern env ([],[])) lhs) in
+	  List.split (List.map (ast_to_pattern scopes ([],[])) lhs) in
 	let idsl, substl = List.split (List.flatten idsl_substl_list) in
 	let eqn_ids = List.flatten idsl in
 	let subst = List.flatten substl in 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 2d7c966ecc..d72a06f2a2 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -494,6 +494,7 @@ let gecdyn s =
   Hashtbl.add (snd uconstr) s (inDynamicAstType e); e
 
 let dynconstr = gecdyn "dynconstr"
+let dyncasespattern = gecdyn "dyncasespattern"
 let dyntactic = gecdyn "dyntactic"
 let dynvernac = gecdyn "dynvernac"
 let dynastlist = gecdyn "dynastlist"
@@ -504,6 +505,7 @@ let set_globalizer f = globalizer := f
 
 GEXTEND Gram
   dynconstr: [ [ a = Constr.constr -> !globalizer (PureAstNode a) ] ];
+  dyncasespattern: [ [ a = Constr.pattern -> !globalizer (PureAstNode a) ] ];
 (*
   dyntactic: [ [ a = Tactic.tactic -> !globalizer (TacticAstNode a) ] ];
   dynvernac: [ [ a = Vernac_.vernac -> !globalizer(VernacAstNode a) ] ];
@@ -520,6 +522,7 @@ type parser_type =
   | AstListParser
   | AstParser
   | ConstrParser
+  | CasesPatternParser
   | TacticParser
   | VernacParser
 
@@ -539,6 +542,7 @@ let entry_type_of_parser =  function
 
 let parser_type_from_name =  function
   | "constr" -> ConstrParser
+  | "cases_pattern" -> CasesPatternParser
   | "tactic" -> TacticParser
   | "vernac" -> VernacParser
   | s -> AstParser
@@ -547,6 +551,7 @@ let set_default_action_parser = function
   | AstListParser -> default_action_parser_ref := dynastlist
   | AstParser -> default_action_parser_ref := dynast
   | ConstrParser  -> default_action_parser_ref := dynconstr
+  | CasesPatternParser  -> default_action_parser_ref := dyncasespattern
   | TacticParser -> default_action_parser_ref := dyntactic
   | VernacParser -> default_action_parser_ref := dynvernac
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f6bd506375..eb49b403c6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -76,6 +76,7 @@ type parser_type =
   | AstListParser
   | AstParser
   | ConstrParser
+  | CasesPatternParser
   | TacticParser
   | VernacParser