Getting rid of IntroPatternArgType.

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

12 files changed, 42 insertions, 46 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a9b942e7bb..9d6b4886b5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -352,7 +352,6 @@ let pploc x = let (l,r) = Loc.unloc x in
 let rec pr_argument_type = function
   (* Basic types *)
   | IntOrVarArgType -> str"int-or-var"
-  | IntroPatternArgType -> str"intro-pattern"
   | IdentArgType true -> str"ident"
   | IdentArgType false -> str"pattern_ident"
   | VarArgType -> str"var"
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index fd18dfdf1f..57cde5c8cd 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -34,7 +34,6 @@ let mk_extraarg s =
 
 let rec make_wit loc = function
   | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
-  | IntroPatternArgType -> <:expr< Constrarg.wit_intro_pattern >>
   | IdentArgType b -> <:expr< Constrarg.wit_ident_gen $mlexpr_of_bool b$ >>
   | VarArgType -> <:expr< Constrarg.wit_var >>
   | RefArgType -> <:expr< Constrarg.wit_ref >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 65aeef11e1..acb6c8347a 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -203,7 +203,6 @@ let mlexpr_of_red_expr = function
 let rec mlexpr_of_argtype loc = function
   | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
   | Genarg.RefArgType -> <:expr< Genarg.RefArgType >>
-  | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >>
   | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 540bca62e6..87da56e4fc 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -32,7 +32,8 @@ let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type =
 
 let wit_int_or_var = unsafe_of_type IntOrVarArgType
 
-let wit_intro_pattern = unsafe_of_type IntroPatternArgType
+let wit_intro_pattern : intro_pattern_expr located uniform_genarg_type =
+  Genarg.make0 None "intropattern"
 
 let wit_ident_gen b = unsafe_of_type (IdentArgType b)
 
@@ -65,3 +66,7 @@ let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
 let wit_bindings = unsafe_of_type BindingsArgType
 
 let wit_red_expr = unsafe_of_type RedExprArgType
+
+(** Register location *)
+
+let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 86ac93d897..df4ed2c41e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -188,7 +188,6 @@ and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
   | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
-  | IntroPattern   of intro_pattern_expr located
   | Reference      of 'ref
   | TacCall of Loc.t * 'ref *
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg list
diff --git a/lib/genarg.ml b/lib/genarg.ml
index dbde4652c7..77c8922a0a 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -12,7 +12,6 @@ open Util
 type argument_type =
   (* Basic types *)
   | IntOrVarArgType
-  | IntroPatternArgType
   | IdentArgType of bool
   | VarArgType
   | RefArgType
@@ -34,7 +33,6 @@ type argument_type =
 
 let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | IntOrVarArgType, IntOrVarArgType -> true
-| IntroPatternArgType, IntroPatternArgType -> true
 | IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2
 | VarArgType, VarArgType -> true
 | RefArgType, RefArgType -> true
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 14133fff03..d395136af7 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -181,7 +181,6 @@ val app_pair :
 type argument_type =
   (** Basic types *)
   | IntOrVarArgType
-  | IntroPatternArgType
   | IdentArgType of bool
   | VarArgType
   | RefArgType
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index b612676e1d..e0a1c046a4 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -27,6 +27,7 @@ let arg_of_expr = function
 
 let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
 let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
+let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
 
 (* Tactics grammar rules *)
 
@@ -98,7 +99,7 @@ GEXTEND Gram
       | IDENT "constr"; ":"; c = Constr.constr ->
           TacArg(!@loc,ConstrMayEval(ConstrTerm c))
       | IDENT "ipattern"; ":"; ipat = simple_intropattern ->
-	  TacArg(!@loc,IntroPattern ipat)
+	  TacArg(!@loc, TacGeneric (genarg_of_ipattern ipat))
       | r = reference; la = LIST0 tactic_arg ->
           TacArg(!@loc,TacCall (!@loc,r,la)) ]
     | "0"
@@ -119,7 +120,8 @@ GEXTEND Gram
   tactic_arg:
     [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
       | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n)
-      | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat
+      | IDENT "ipattern"; ":"; ipat = simple_intropattern ->
+        TacGeneric (genarg_of_ipattern ipat)
       | a = may_eval_arg -> a
       | r = reference -> Reference r
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 1bf6970745..3b3de2a3c7 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -143,7 +143,6 @@ let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
 let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
   match Genarg.genarg_tag x with
   | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
-  | IntroPatternArgType -> pr_intro_pattern (out_gen (rawwit wit_intro_pattern) x)
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
   | RefArgType -> prref (out_gen (rawwit wit_ref) x)
@@ -183,7 +182,6 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
 let rec pr_glb_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
   | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
-  | IntroPatternArgType -> pr_intro_pattern (out_gen (glbwit wit_intro_pattern) x)
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
   | RefArgType -> pr_or_var (pr_located pr_global) (out_gen (glbwit wit_ref) x)
@@ -224,7 +222,6 @@ let rec pr_glb_generic prc prlc prtac prpat x =
 let rec pr_top_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
   | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
-  | IntroPatternArgType -> pr_intro_pattern (out_gen (topwit wit_intro_pattern) x)
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x)
   | VarArgType -> pr_id (out_gen (topwit wit_var) x)
   | RefArgType -> pr_global (out_gen (topwit wit_ref) x)
@@ -943,7 +940,6 @@ and pr_tacarg = function
       pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
   | MetaIdArg (loc,true,s) -> pr_with_comments loc (str ("$" ^ s))
   | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s))
-  | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
   | Reference r -> pr_ref r
   | ConstrMayEval c -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c
   | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
@@ -1007,6 +1003,14 @@ let pr_glob_tactic_level env =
 
 let pr_glob_tactic env = pr_glob_tactic_level env ltop
 
+(** Registering *)
+
+let register_uniform_printer wit pr =
+  Genprint.register_print0 wit pr pr pr
+
+let () = Genprint.register_print0 Constrarg.wit_intro_pattern
+  pr_intro_pattern pr_intro_pattern pr_intro_pattern
+
 let _ = Hook.set Tactic_debug.tactic_printer
   (fun x -> pr_glob_tactic (Global.env()) x)
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 3f52de11ce..c449cab8d9 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -263,7 +263,9 @@ let intern_non_tactic_reference strict ist r =
   with Not_found ->
   (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
   match r with
-  | Ident (loc,id) when not strict -> IntroPattern (loc,IntroIdentifier id)
+  | Ident (loc,id) when not strict ->
+    let ipat = in_gen (glbwit wit_intro_pattern) (loc, IntroIdentifier id) in
+    TacGeneric ipat
   | _ ->
   (* Reference not found *)
   error_global_not_found_loc (qualid_of_reference r)
@@ -691,7 +693,7 @@ and intern_tactic_as_arg loc onlytac ist a =
   | TacCall _ | TacExternal _ | Reference _
   | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
-  | IntroPattern _ | ConstrMayEval _ | TacFreshId _ as a ->
+  | ConstrMayEval _ | TacFreshId _ as a ->
       if onlytac then error_tactic_expected loc else TacArg (loc,a)
   | MetaIdArg _ -> assert false
 
@@ -706,9 +708,6 @@ and intern_tactic_fun ist (var,body) =
 
 and intern_tacarg strict onlytac ist = function
   | Reference r -> intern_non_tactic_reference strict ist r
-  | IntroPattern ipat ->
-      let lf = ref([],[]) in (*How to know what names the intropattern binds?*)
-      IntroPattern (intern_intro_pattern lf ist ipat)
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
   | MetaIdArg (loc,istac,s) ->
       (* $id can occur in Grammar tactic... *)
@@ -754,11 +753,6 @@ and intern_genarg ist x =
   | IntOrVarArgType ->
       in_gen (glbwit wit_int_or_var)
         (intern_or_var ist (out_gen (rawwit wit_int_or_var) x))
-  | IntroPatternArgType ->
-      let lf = ref ([],[]) in
-      (* how to know which names are bound by the intropattern *)
-      in_gen (glbwit wit_intro_pattern)
-        (intern_intro_pattern lf ist (out_gen (rawwit wit_intro_pattern) x))
   | IdentArgType b ->
       let lf = ref ([],[]) in
       in_gen (glbwit (wit_ident_gen b))
@@ -941,6 +935,17 @@ let add_tacdef local isrec tacl =
 				   else str " is defined")))
     tacl
 
+(** Registering *)
+
+let () =
+  let intern_intro_pattern ist pat =
+    let lf = ref ([], []) in
+    let ans = intern_intro_pattern lf ist pat in
+    let ist = { ist with ltacvars = !lf } in
+    (ist, ans)
+  in
+  Genintern.register_intern0 wit_intro_pattern intern_intro_pattern
+
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index de72f2b5c8..05a62e499e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1099,9 +1099,6 @@ and interp_tacarg ist gl arg =
       let (sigma,v) = interp_ltac_reference dloc false ist gl r in
       evdref := sigma;
       v
-    | IntroPattern ipat ->
-      let ans = interp_intro_pattern ist gl ipat in
-      in_gen (topwit wit_intro_pattern) ans
     | ConstrMayEval c ->
       let (sigma,c_interp) = interp_constr_may_eval ist gl c in
       evdref := sigma;
@@ -1369,9 +1366,6 @@ and interp_genarg ist gl x =
     | IntOrVarArgType ->
       in_gen (topwit wit_int_or_var)
         (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x)))
-    | IntroPatternArgType ->
-      in_gen (topwit wit_intro_pattern)
-        (interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x))
     | IdentArgType b ->
       in_gen (topwit (wit_ident_gen b))
         (pf_interp_fresh_ident ist gl (out_gen (glbwit (wit_ident_gen b)) x))
@@ -1879,9 +1873,6 @@ and interp_atomic ist gl tac =
     let rec f x = match genarg_tag x with
     | IntOrVarArgType ->
         mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)
-    | IntroPatternArgType ->
-	let ipat = interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x) in
-	in_gen (topwit wit_intro_pattern) ipat
     | IdentArgType b ->
 	value_of_ident (interp_fresh_ident ist env
 	  (out_gen (glbwit (wit_ident_gen b)) x))
@@ -1935,11 +1926,6 @@ and interp_atomic ist gl tac =
 	let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
 	let ans = List.map mk_ident (out_gen wit x) in
         in_gen (topwit (wit_list0 wit_genarg)) ans
-    | List0ArgType IntroPatternArgType ->
-        let wit = glbwit (wit_list0 wit_intro_pattern) in
-	let mk_ipat x = interp_intro_pattern ist gl x in
-	let ans = List.map mk_ipat (out_gen wit x) in
-        in_gen (topwit (wit_list0 wit_intro_pattern)) ans
     | List1ArgType ConstrArgType ->
         let wit = glbwit (wit_list1 wit_constr) in
 	let (sigma, l_interp) =
@@ -1963,11 +1949,6 @@ and interp_atomic ist gl tac =
 	let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
 	let ans = List.map mk_ident (out_gen wit x) in
         in_gen (topwit (wit_list1 wit_genarg)) ans
-    | List1ArgType IntroPatternArgType ->
-        let wit = glbwit (wit_list1 wit_intro_pattern) in
-	let mk_ipat x = interp_intro_pattern ist gl x in
-	let ans = List.map mk_ipat (out_gen wit x) in
-        in_gen (topwit (wit_list1 wit_intro_pattern)) ans
     | List0ArgType _ -> app_list0 f x
     | List1ArgType _ -> app_list1 f x
     | ExtraArgType _ ->
@@ -2059,6 +2040,10 @@ let () =
 let () =
   declare_uniform wit_pre_ident str
 
+let () =
+  let interp ist gl pat = (gl.sigma, interp_intro_pattern ist gl pat) in
+  Geninterp.register_interp0 wit_intro_pattern interp
+
 (***************************************************************************)
 (* Other entry points *)
 
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 274c3b352a..2e84d44258 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -264,7 +264,7 @@ and subst_tacarg subst = function
       TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
   | TacExternal (_loc,com,req,la) ->
       TacExternal (_loc,com,req,List.map (subst_tacarg subst) la)
-  | (IntroPattern _ | TacFreshId _) as x -> x
+  | TacFreshId _ as x -> x
   | Tacexp t -> Tacexp (subst_tactic subst t)
   | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg)
   | TacDynamic(the_loc,t) as x ->
@@ -289,8 +289,6 @@ and subst_match_rule subst = function
 and subst_genarg subst (x:glob_generic_argument) =
   match genarg_tag x with
   | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (out_gen (glbwit wit_int_or_var) x)
-  | IntroPatternArgType ->
-      in_gen (glbwit wit_intro_pattern) (out_gen (glbwit wit_intro_pattern) x)
   | IdentArgType b ->
       in_gen (glbwit (wit_ident_gen b)) (out_gen (glbwit (wit_ident_gen b)) x)
   | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
@@ -332,4 +330,8 @@ and subst_genarg subst (x:glob_generic_argument) =
       | None ->
           Genintern.generic_substitute subst x
 
+(** Registering *)
+
+let () = Genintern.register_subst0 wit_intro_pattern (fun _ v -> v)
+
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic