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

14 files changed, 160 insertions, 101 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 80248f7e5..4ef21df45 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -8,8 +8,10 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
+open Nameops
 open Nametab
 open Rawterm
 open Topconstr
@@ -22,6 +24,7 @@ type argument_type =
   | IntOrVarArgType
   | StringArgType
   | PreIdentArgType
+  | IntroPatternArgType
   | IdentArgType
   | RefArgType
   (* Specific types *)
@@ -61,6 +64,25 @@ let create_arg s =
 
 let exists_argtype s = List.mem s !dyntab
 
+type intro_pattern_expr =
+  | IntroOrAndPattern of case_intro_pattern_expr
+  | IntroWildcard
+  | IntroIdentifier of identifier
+and case_intro_pattern_expr = intro_pattern_expr list list
+
+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 = function
+  | [_::_ as pl] ->
+      str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
+  | pll ->
+      str "[" ++
+      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+      ++ str "]"
+
 type open_constr = Evd.evar_map * Term.constr
 type open_constr_expr = constr_expr
 type open_rawconstr = rawconstr_and_expr
@@ -81,14 +103,18 @@ let rawwit_string = StringArgType
 let globwit_string = StringArgType
 let wit_string = StringArgType
 
-let rawwit_ident = IdentArgType
-let globwit_ident = IdentArgType
-let wit_ident = IdentArgType
-
 let rawwit_pre_ident = PreIdentArgType
 let globwit_pre_ident = PreIdentArgType
 let wit_pre_ident = PreIdentArgType
 
+let rawwit_intro_pattern = IntroPatternArgType
+let globwit_intro_pattern = IntroPatternArgType
+let wit_intro_pattern = IntroPatternArgType
+
+let rawwit_ident = IdentArgType
+let globwit_ident = IdentArgType
+let wit_ident = IdentArgType
+
 let rawwit_ref = RefArgType
 let globwit_ref = RefArgType
 let wit_ref = RefArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 23e1b5377..18f1e33fb 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -28,6 +28,15 @@ type open_constr = Evd.evar_map * Term.constr
 type open_constr_expr = constr_expr
 type open_rawconstr = rawconstr_and_expr
 
+type intro_pattern_expr =
+  | IntroOrAndPattern of case_intro_pattern_expr
+  | IntroWildcard
+  | IntroIdentifier of identifier
+and case_intro_pattern_expr = intro_pattern_expr list list
+
+val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
+val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
+
 (* The route of a generic argument, from parsing to evaluation
 
               parsing        in_raw                           out_raw
@@ -52,8 +61,9 @@ BoolArgType                    bool                     bool
 IntArgType                     int                      int
 IntOrVarArgType                int or_var               int
 StringArgType                  string (parsed w/ "")    string
-IdentArgType                   identifier               identifier         
 PreIdentArgType                string (parsed w/o "")   string
+IdentArgType                   identifier               identifier         
+IntroPatternArgType            intro_pattern_expr       intro_pattern_expr
 RefArgType                     reference                global_reference
 ConstrArgType                  constr_expr              constr
 ConstrMayEvalArgType           constr_expr may_eval     constr
@@ -85,14 +95,18 @@ val rawwit_string : (string,'co,'ta) abstract_argument_type
 val globwit_string : (string,'co,'ta) abstract_argument_type
 val wit_string : (string,'co,'ta) abstract_argument_type
 
-val rawwit_ident : (identifier,'co,'ta) abstract_argument_type
-val globwit_ident : (identifier,'co,'ta) abstract_argument_type
-val wit_ident : (identifier,'co,'ta) abstract_argument_type
-
 val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type
 val globwit_pre_ident : (string,'co,'ta) abstract_argument_type
 val wit_pre_ident : (string,'co,'ta) abstract_argument_type
 
+val rawwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+val globwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+val wit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+
+val rawwit_ident : (identifier,'co,'ta) abstract_argument_type
+val globwit_ident : (identifier,'co,'ta) abstract_argument_type
+val wit_ident : (identifier,'co,'ta) abstract_argument_type
+
 val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type
 val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_ref : (global_reference,constr,'ta) abstract_argument_type
@@ -198,6 +212,7 @@ type argument_type =
   | IntOrVarArgType
   | StringArgType
   | PreIdentArgType
+  | IntroPatternArgType
   | IdentArgType
   | RefArgType
   (* Specific types *)
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 44a54a0cf..6ed6c51e4 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 1e57506df..bd60dc672 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 c57e7761d..35f8e642e 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 e9a5ed777..73718c629 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 4cdf0bc35..721697c9a 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 296c66b07..5aad710c7 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 c245f9fd5..68977fb3d 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 3a6cfab0e..9c27cb65b 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 8df84e573..87eb0784f 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 >>
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fe96fa44d..a0d791a58 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -69,10 +69,10 @@ type value =
   | VFun of (identifier*value) list * identifier option list * glob_tactic_expr
   | VVoid
   | VInteger of int
-  | VIdentifier of identifier (* idents which are not bound, as in "Intro H" *)
-                              (* but which may be bound later, as in "tac" in*)
-                              (* "Intro H; tac" *)
-  | VConstr of constr         (* includes idents known bound and references *)
+  | VIntroPattern of intro_pattern_expr (* includes idents which are not *)
+                        (* bound as in "Intro H" but which may be bound *)
+                        (* later, as in "tac" in "Intro H; tac" *)
+  | VConstr of constr   (* includes idents known bound and references *)
   | VConstr_context of constr
   | VRec of value ref
 
@@ -114,7 +114,7 @@ let constr_of_VConstr_context = function
 let pr_value env = function
   | VVoid -> str "()"
   | VInteger n -> int n
-  | VIdentifier id -> pr_id id
+  | VIntroPattern ipat -> pr_intro_pattern ipat
   | VConstr c -> Printer.prterm_env env c
   | VConstr_context c -> Printer.prterm_env env c
   | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "<fun>"
@@ -205,7 +205,6 @@ let coerce_to_reference env = function
   | VConstr c ->
       (try reference_of_constr c
       with Not_found -> invalid_arg_loc (loc, "Not a reference"))
-(*  | VIdentifier id -> VarRef id*)
   | v -> errorlabstrm "coerce_to_reference"
       (str "The value" ++ spc () ++ pr_value env v ++ 
        str "cannot be coerced to a reference")
@@ -220,7 +219,6 @@ let coerce_to_evaluable_ref env c =
   let ev = match c with
     | VConstr c when isConst c -> EvalConstRef (destConst c)
     | VConstr c when isVar c -> EvalVarRef (destVar c)
-(*    | VIdentifier id -> EvalVarRef id*)
     | _ -> error_not_evaluable (pr_value env c)
   in
   if not (Tacred.is_evaluable env ev) then
@@ -352,7 +350,7 @@ let find_hyp id sign =
 (* be fresh in which case it is binding later on *)
 let intern_ident l ist id =
   (* We use identifier both for variables and new names; thus nothing to do *)
-  if find_ident id ist then () else l:=(id::fst !l,id::snd !l);
+  if not (find_ident id ist) then l:=(id::fst !l,id::snd !l);
   id
 
 let intern_name l ist = function
@@ -442,7 +440,8 @@ let intern_reference strict ist = function
           ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
         with Not_found ->
           (match r with
-            | Ident (loc,id) when not strict -> Identifier id
+            | Ident (loc,id) when not strict -> 
+		IntroPattern (IntroIdentifier id)
             | _ ->
                 let (loc,qid) = qualid_of_reference r in
                 error_global_not_found_loc loc qid)))
@@ -795,7 +794,9 @@ and intern_tactic_fun ist (var,body) =
 and intern_tacarg strict ist = function
   | TacVoid -> TacVoid
   | Reference r -> intern_reference strict ist r
-  | Identifier id -> anomaly "Not used only in raw_tactic_expr"
+  | IntroPattern ipat -> 
+      let lf = ref([],[]) in (*How to know what names the intropattern binds?*)
+      IntroPattern (intern_intro_pattern lf ist ipat)
   | Integer n -> Integer n
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
   | MetaIdArg (loc,s) ->
@@ -840,6 +841,11 @@ and intern_genarg ist x =
       in_gen globwit_string (out_gen rawwit_string x)
   | PreIdentArgType ->
       in_gen globwit_pre_ident (out_gen rawwit_pre_ident x)
+  | IntroPatternArgType ->
+      let lf = ref ([],[]) in
+      (* how to know which names are bound by the intropattern *)
+      in_gen globwit_intro_pattern
+        (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x))
   | IdentArgType ->
       in_gen globwit_ident (snd (intern_hyp ist (dummy_loc,out_gen rawwit_ident x)))
   | RefArgType ->
@@ -962,7 +968,8 @@ let apply_matching pat csr =
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
 let apply_one_mhyp_context ist env gl lmatch (hypname,pat) (lhyps,nocc) =
   let get_id_couple id = function
-    | Name idpat -> [idpat,VIdentifier id]
+(*    | Name idpat -> [idpat,VIdentifier id]*)
+    | Name idpat -> [idpat,VConstr (mkVar id)]
     | Anonymous -> [] in
   let rec apply_one_mhyp_context_rec nocc = function
     | (id,hyp)::tl as hyps ->
@@ -1009,31 +1016,43 @@ let set_debug pos = debug := pos
 let get_debug () = !debug
 
 (* Interprets an identifier which must be fresh *)
-let eval_ident ist id =
+let interp_ident ist id =
   try match List.assoc id ist.lfun with
-  | VIdentifier id -> id
+  | VIntroPattern (IntroIdentifier id) -> id
   | VConstr c as v when isVar c ->
       (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *)
       (* c is then expected not to belong to the proof context *)
-      (* would be checkable if env were known from eval_ident *)
+      (* would be checkable if env were known from interp_ident *)
       destVar c
-  | _ -> user_err_loc(loc,"eval_ident", str "An ltac name (" ++ pr_id id ++ 
+  | _ -> user_err_loc(loc,"interp_ident", str "An ltac name (" ++ pr_id id ++ 
          str ") should have been bound to an identifier")
   with Not_found -> id
 
-let eval_integer lfun (loc,id) =
+let interp_intro_pattern_var ist id =
+  try match List.assoc id ist.lfun with
+  | VIntroPattern ipat -> ipat
+  | VConstr c as v when isVar c ->
+      (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *)
+      (* c is then expected not to belong to the proof context *)
+      (* would be checkable if env were known from interp_ident *)
+      IntroIdentifier (destVar c)
+  | _ -> user_err_loc(loc,"interp_ident", str "An ltac name (" ++ pr_id id ++ 
+         str ") should have been bound to an introduction pattern")
+  with Not_found -> IntroIdentifier id
+
+let interp_int lfun (loc,id) =
   try match List.assoc id lfun with
   | VInteger n -> n
-  | _ -> user_err_loc(loc,"eval_integer",str "should be bound to an integer")
-  with Not_found -> user_err_loc (loc,"eval_integer",str "Unbound variable")
+  | _ -> user_err_loc(loc,"interp_int",str "should be bound to an integer")
+  with Not_found -> user_err_loc (loc,"interp_int",str "Unbound variable")
 
 let interp_int_or_var ist = function
-  | ArgVar locid -> eval_integer ist.lfun locid
+  | ArgVar locid -> interp_int ist.lfun locid
   | ArgArg n -> n
 
 let constr_of_value env = function
   | VConstr csr -> csr
-  | VIdentifier id -> constr_of_id env id
+  | VIntroPattern (IntroIdentifier id) -> constr_of_id env id
   | _ -> raise Not_found
 
 let is_variable env id =
@@ -1041,7 +1060,7 @@ let is_variable env id =
 
 let variable_of_value env = function
   | VConstr c as v when isVar c -> destVar c
-  | VIdentifier id' when is_variable env id' -> id'
+  | VIntroPattern (IntroIdentifier id) when is_variable env id -> id
   | _ -> raise Not_found
 
 (* Extract a variable from a value, if any *)
@@ -1069,9 +1088,9 @@ let interp_var ist gl (loc,id) =
 (* Interprets an existing hypothesis (i.e. a declared variable) *)
 let interp_hyp = interp_var
 
-let eval_name ist = function
+let interp_name ist = function
   | Anonymous -> Anonymous
-  | Name id -> Name (eval_ident ist id)
+  | Name id -> Name (interp_ident ist id)
 
 let interp_clause_pattern ist gl (l,occl) =
   let rec check acc = function
@@ -1083,20 +1102,7 @@ let interp_clause_pattern ist gl (l,occl) =
     | [] -> []
   in (l,check [] occl)
 
-let interp_pure_qualid is_applied env (loc,qid) =
-  try VConstr (constr_of_reference (find_reference env qid))
-  with Not_found ->
-    let (dir,id) = repr_qualid qid in
-    if not is_applied & dir = empty_dirpath then VIdentifier id
-    else user_err_loc (loc,"interp_pure_qualid",str "Unknown reference")
-
 (* Interprets a qualified name *)
-let eval_ref ist env = function
-  | Qualid locqid -> interp_pure_qualid false env locqid
-  | Ident (loc,id) ->
-      try unrec (List.assoc id ist.lfun)
-      with Not_found -> interp_pure_qualid false env (loc,make_short_qualid id)
-
 let interp_reference ist env = function
   | ArgArg (_,r) -> r
   | ArgVar (loc,id) -> coerce_to_reference env (unrec (List.assoc id ist.lfun))
@@ -1129,8 +1135,6 @@ let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
     onconcl=b;
     concl_occs=occs }
 
-let eval_opt_ident ist = option_app (eval_ident ist)
-
 (* Interpretation of constructions *)
 
 (* Extract the constr list from lfun *)
@@ -1139,14 +1143,23 @@ let rec constr_list_aux env = function
       let (l1,l2) = constr_list_aux env tl in
       (try ((id,constr_of_value env v)::l1,l2)
        with Not_found -> 
-	 (l1,(id,match v with VIdentifier id0 -> Some id0 | _ -> None)::l2))
+	 let ido = match v with
+	   | VIntroPattern (IntroIdentifier id0) -> Some id0
+	   | _ -> None in
+	 (l1,(id,ido)::l2))
   | [] -> ([],[])
 
 let constr_list ist env = constr_list_aux env ist.lfun
 
-(* Extract the identifier list from lfun *)
+(*Extract the identifier list from lfun: join all branches (what to do else?)*)
+let rec intropattern_ids = function
+  | IntroIdentifier id -> [id]
+  | IntroOrAndPattern ll -> 
+      List.flatten (List.map intropattern_ids (List.flatten ll))
+  | IntroWildcard -> []
+
 let rec extract_ids = function
-  | (id,VIdentifier id')::tl -> id'::extract_ids tl
+  | (id,VIntroPattern ipat)::tl -> intropattern_ids ipat @ extract_ids tl
   | _::tl -> extract_ids tl
   | [] -> []
 
@@ -1246,7 +1259,7 @@ let interp_constr_may_eval ist gl c =
 let rec interp_intro_pattern ist = function
   | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist l)
   | IntroWildcard -> IntroWildcard
-  | IntroIdentifier id -> IntroIdentifier (eval_ident ist id)
+  | IntroIdentifier id -> interp_intro_pattern_var ist id
 
 and interp_case_intro_pattern ist =
   List.map (List.map (interp_intro_pattern ist))
@@ -1258,7 +1271,7 @@ let interp_quantified_hypothesis ist gl = function
   | NamedHyp id ->
       try match List.assoc id ist.lfun with
 	| VInteger n -> AnonHyp n
-	| VIdentifier id -> NamedHyp id
+(*	| VIdentifier id -> NamedHyp id   Why ?*)
 	| v -> NamedHyp (variable_of_value (pf_env gl) v)
       with Not_found -> NamedHyp id
 
@@ -1337,7 +1350,7 @@ and interp_tacarg ist gl = function
   | TacVoid -> VVoid
   | Reference r -> interp_ltac_reference false ist gl r
   | Integer n -> VInteger n
-  | Identifier id -> VIdentifier id
+  | IntroPattern ipat -> VIntroPattern ipat
   | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c)
   | MetaIdArg (loc,id) -> assert false
   | TacCall (loc,f,l) ->
@@ -1347,7 +1360,8 @@ and interp_tacarg ist gl = function
       interp_app ist gl fv largs loc
   | TacFreshId idopt -> 
       let s = match idopt with None -> "H" | Some s -> s in
-      VIdentifier (Tactics.fresh_id (extract_ids ist.lfun) (id_of_string s) gl)
+      let id = Tactics.fresh_id (extract_ids ist.lfun) (id_of_string s) gl in
+      VIntroPattern (IntroIdentifier id)
   | Tacexp t -> val_interp ist gl t
   | TacDynamic(_,t) ->
       let tg = (tag t) in
@@ -1553,8 +1567,11 @@ and interp_genarg ist goal x =
       in_gen wit_string (out_gen globwit_string x)
   | PreIdentArgType ->
       in_gen wit_pre_ident (out_gen globwit_pre_ident x)
+  | IntroPatternArgType ->
+      in_gen wit_intro_pattern
+        (interp_intro_pattern ist (out_gen globwit_intro_pattern x))
   | IdentArgType ->
-      in_gen wit_ident (eval_ident ist (out_gen globwit_ident x))
+      in_gen wit_ident (interp_ident ist (out_gen globwit_ident x))
   | RefArgType ->
       in_gen wit_ref (pf_interp_reference ist goal (out_gen globwit_ref x))
   | SortArgType ->
@@ -1640,7 +1657,7 @@ and interp_atomic ist gl = function
   | TacIntrosUntil hyp ->
       h_intros_until (interp_quantified_hypothesis ist gl hyp)
   | TacIntroMove (ido,ido') ->
-      h_intro_move (option_app (eval_ident ist) ido)
+      h_intro_move (option_app (interp_ident ist) ido)
       (option_app (interp_hyp ist gl) ido')
   | TacAssumption -> h_assumption
   | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
@@ -1651,24 +1668,24 @@ and interp_atomic ist gl = function
   | TacElimType c -> h_elim_type (pf_interp_constr ist gl c)
   | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb)
   | TacCaseType c -> h_case_type (pf_interp_constr ist gl c)
-  | TacFix (idopt,n) -> h_fix (eval_opt_ident ist idopt) n
+  | TacFix (idopt,n) -> h_fix (option_app (interp_ident ist) idopt) n
   | TacMutualFix (id,n,l) ->
-      let f (id,n,c) = (eval_ident ist id,n,pf_interp_constr ist gl c) in
-      h_mutual_fix (eval_ident ist id) n (List.map f l)
-  | TacCofix idopt -> h_cofix (eval_opt_ident ist idopt)
+      let f (id,n,c) = (interp_ident ist id,n,pf_interp_constr ist gl c) in
+      h_mutual_fix (interp_ident ist id) n (List.map f l)
+  | TacCofix idopt -> h_cofix (option_app (interp_ident ist) idopt)
   | TacMutualCofix (id,l) ->
-      let f (id,c) = (eval_ident ist id,pf_interp_constr ist gl c) in
-      h_mutual_cofix (eval_ident ist id) (List.map f l)
+      let f (id,c) = (interp_ident ist id,pf_interp_constr ist gl c) in
+      h_mutual_cofix (interp_ident ist id) (List.map f l)
   | TacCut c -> h_cut (pf_interp_constr ist gl c)
   | TacTrueCut (na,c) ->
-      h_true_cut (eval_name ist na) (pf_interp_constr ist gl c)
+      h_true_cut (interp_name ist na) (pf_interp_constr ist gl c)
   | TacForward (b,na,c) ->
-      h_forward b (eval_name ist na) (pf_interp_constr ist gl c)
+      h_forward b (interp_name ist na) (pf_interp_constr ist gl c)
   | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
   | TacLetTac (na,c,clp) ->
       let clp = interp_clause ist gl clp in
-      h_let_tac (eval_name ist na) (pf_interp_constr ist gl c) clp
+      h_let_tac (interp_name ist na) (pf_interp_constr ist gl c) clp
   | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c)
       (clause_app (interp_hyp_location ist gl) ido)
 
@@ -1713,7 +1730,7 @@ and interp_atomic ist gl = function
   | TacMove (dep,id1,id2) ->
       h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2)
   | TacRename (id1,id2) ->
-      h_rename (interp_hyp ist gl id1) (eval_ident ist (snd id2))
+      h_rename (interp_hyp ist gl id1) (interp_ident ist (snd id2))
 
   (* Constructors *)
   | TacLeft bl -> h_left (interp_bindings ist gl bl)
@@ -1761,7 +1778,10 @@ and interp_atomic ist gl = function
     | IntOrVarArgType -> 
 	VInteger (interp_int_or_var ist (out_gen globwit_int_or_var x))
     | PreIdentArgType ->
-        VIdentifier (id_of_string (out_gen globwit_pre_ident x))
+        VIntroPattern
+	  (IntroIdentifier (id_of_string (out_gen globwit_pre_ident x)))
+    | IntroPatternArgType ->
+	VIntroPattern (out_gen globwit_intro_pattern x)
     | IdentArgType -> 
 	VConstr 
 	  (mkVar (interp_hyp ist gl (dummy_loc,out_gen globwit_ident x)))
@@ -2020,7 +2040,7 @@ and subst_tacarg subst = function
   | MetaIdArg (_loc,_) -> assert false
   | TacCall (_loc,f,l) ->
       TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
-  | (TacVoid | Identifier _ | Integer _ | TacFreshId _) as x -> x
+  | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x
   | Tacexp t -> Tacexp (subst_tactic subst t)
   | TacDynamic(_,t) as x ->
       (match tag t with
@@ -2046,6 +2066,8 @@ and subst_genarg subst (x:glob_generic_argument) =
   | IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x)
   | StringArgType -> in_gen globwit_string (out_gen globwit_string x)
   | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x)
+  | IntroPatternArgType ->
+      in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x)
   | IdentArgType -> in_gen globwit_ident (out_gen globwit_ident x)
   | RefArgType ->
       in_gen globwit_ref (subst_global_reference subst 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 1a80e9811..49af044c5 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -28,7 +28,7 @@ type value =
   | VFun of (identifier * value) list * identifier option list * glob_tactic_expr
   | VVoid
   | VInteger of int
-  | VIdentifier of identifier
+  | VIntroPattern of intro_pattern_expr
   | VConstr of constr
   | VConstr_context of constr
   | VRec of value ref
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index d663c942a..5704d853b 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -207,19 +207,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 = function
-  | [_::_ as pl] ->
-      str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
-  | 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)
@@ -765,7 +752,7 @@ and pr_tacarg env = function
   | TacDynamic (loc,t) ->
       pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
   | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
-  | Identifier id -> pr_id id
+  | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
   | ConstrMayEval c ->