Getting rid of IntroPatternArgType.

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

3 files changed, 24 insertions, 32 deletions

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