Généralisation du type ltac Identifier en IntroPattern; prise en compte des IntroPattern au parsing, à l'interprétation, à la traduction

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

9 files changed, 27 insertions, 18 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 44a54a0cff..6ed6c51e49 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -23,6 +23,7 @@ let rec make_rawwit loc = function
   | IntOrVarArgType -> <:expr< Genarg.rawwit_int_or_var >>
   | StringArgType -> <:expr< Genarg.rawwit_string >>
   | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >>
+  | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >>
   | IdentArgType -> <:expr< Genarg.rawwit_ident >>
   | RefArgType -> <:expr< Genarg.rawwit_ref >>
   | SortArgType -> <:expr< Genarg.rawwit_sort >>
@@ -47,6 +48,7 @@ let rec make_globwit loc = function
   | IntOrVarArgType -> <:expr< Genarg.globwit_int_or_var >>
   | StringArgType -> <:expr< Genarg.globwit_string >>
   | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >>
+  | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >>
   | IdentArgType -> <:expr< Genarg.globwit_ident >>
   | RefArgType -> <:expr< Genarg.globwit_ref >>
   | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >>
@@ -71,6 +73,7 @@ let rec make_wit loc = function
   | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >>
   | StringArgType -> <:expr< Genarg.wit_string >>
   | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >>
+  | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >>
   | IdentArgType -> <:expr< Genarg.wit_ident >>
   | RefArgType -> <:expr< Genarg.wit_ref >>
   | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 1e57506df1..bd60dc6724 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -188,6 +188,7 @@ GEXTEND Gram
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
       | IDENT "FreshId"; s = OPT STRING -> TacFreshId s
+      | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat
       | r = reference -> Reference r
       | ta = tactic_arg0 -> ta ] ]
   ;
@@ -199,6 +200,7 @@ GEXTEND Gram
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
       | IDENT "FreshId"; s = OPT STRING -> TacFreshId s
+      | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat
       | r = reference; la = LIST1 tactic_arg0 -> TacCall (loc,r,la)
       | r = reference -> Reference r
       | ta = tactic_arg0 -> ta ] ]
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index c57e7761d0..35f8e642e7 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -115,8 +115,10 @@ GEXTEND Gram
 	  s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
       | st = simple_tactic -> TacAtom (loc,st)
       | a = may_eval_arg -> TacArg(a)
-      | IDENT"constr"; ":"; c = Constr.constr ->
+      | IDENT "constr"; ":"; c = Constr.constr ->
           TacArg(ConstrMayEval(ConstrTerm c))
+      | IDENT "ipattern"; ":"; ipat = simple_intropattern -> 
+	  TacArg(IntroPattern ipat)
       | r = reference; la = LIST1 tactic_arg ->
           TacArg(TacCall (loc,r,la))
       | r = reference -> TacArg (Reference r) ]
@@ -127,6 +129,7 @@ GEXTEND Gram
   (* Tactic arguments *)
   tactic_arg:
     [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
+      | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat
       | a = may_eval_arg -> a
       | a = tactic_atom -> a
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ]
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e9a5ed7773..73718c6292 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -64,7 +64,8 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 if !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constrarg bindings constr_with_bindings 
-  quantified_hypothesis red_expr int_or_var castedopenconstr;
+  quantified_hypothesis red_expr int_or_var castedopenconstr
+  simple_intropattern;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 4cdf0bc35c..721697c9a5 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -130,7 +130,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
-  bindings red_expr int_or_var castedopenconstr;
+  bindings red_expr int_or_var castedopenconstr simple_intropattern;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 296c66b07a..5aad710c75 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -379,6 +379,8 @@ module Tactic =
       make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
     let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var"
     let red_expr = make_gen_entry utactic rawwit_red_expr "red_expr"
+    let simple_intropattern = 
+      make_gen_entry utactic rawwit_intro_pattern "simple_intropattern"
 
     (* Main entries for ltac *)
     let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c245f9fd5e..68977fb3d3 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -162,6 +162,7 @@ module Tactic :
     val int_or_var : int or_var Gram.Entry.e
     val red_expr : raw_red_expr Gram.Entry.e
     val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e
+    val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e
     val tactic_arg : raw_tactic_arg Gram.Entry.e
     val tactic : raw_tactic_expr Gram.Entry.e
     val tactic_eoi : raw_tactic_expr Gram.Entry.e
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3a6cfab0e6..9c27cb65b2 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -140,16 +140,6 @@ let pr_with_constr prc = function
   | None -> mt ()
   | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
 
-let rec pr_intro_pattern = function
-  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
-  | IntroWildcard -> str "_"
-  | IntroIdentifier id -> pr_id id
-
-and pr_case_intro_pattern pll =
-  str "[" ++
-  hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
-  ++ str "]"
-
 let pr_with_names = function
   | [] -> mt ()
   | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids)
@@ -265,6 +255,8 @@ let rec pr_raw_generic prc prlc prtac prref x =
   | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen rawwit_int_or_var x)
   | StringArgType -> spc () ++ str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
   | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x)
+  | IntroPatternArgType -> pr_arg pr_intro_pattern 
+      (out_gen rawwit_intro_pattern x)
   | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen rawwit_ident x))
   | RefArgType -> pr_arg prref (out_gen rawwit_ref x)
   | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
@@ -310,6 +302,8 @@ let rec pr_glob_generic prc prlc prtac x =
   | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen globwit_int_or_var x)
   | StringArgType -> spc () ++ str "\"" ++ str (out_gen globwit_string x) ++ str "\""
   | PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x)
+  | IntroPatternArgType ->
+      pr_arg pr_intro_pattern (out_gen globwit_intro_pattern x)
   | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen globwit_ident x))
   | RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x)
   | SortArgType -> pr_arg pr_sort (out_gen globwit_sort x)
@@ -356,6 +350,8 @@ let rec pr_generic prc prlc prtac x =
   | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen wit_int_or_var x)
   | StringArgType -> spc () ++ str "\"" ++ str (out_gen wit_string x) ++ str "\""
   | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x)
+  | IntroPatternArgType -> 
+      pr_arg pr_intro_pattern (out_gen wit_intro_pattern x)
   | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen wit_ident x))
   | RefArgType -> pr_arg pr_global (out_gen wit_ref x)
   | SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x))
@@ -692,7 +688,7 @@ and pr6 = function
 and pr_tacarg0 = function
   | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
   | MetaIdArg (_,s) -> str ("$" ^ s)
-  | Identifier id -> pr_id id
+  | IntroPattern ipat -> pr_intro_pattern ipat
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
   | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 8df84e5736..87eb0784f3 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -133,10 +133,10 @@ let mlexpr_of_reference = function
   | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
 
 let mlexpr_of_intro_pattern = function
-  | Tacexpr.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO"
-  | Tacexpr.IntroWildcard -> <:expr< Tacexpr.IntroWildcard >>
-  | Tacexpr.IntroIdentifier id ->
-      <:expr< Tacexpr.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
+  | Genarg.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO"
+  | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
+  | Genarg.IntroIdentifier id ->
+      <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
 
 let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
 
@@ -250,6 +250,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
   | Genarg.RefArgType -> <:expr< Genarg.RefArgType >>
   | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >>
+  | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >>
   | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
   | Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>