Dead code from August 2014 in apply in.

7 files changed, 17 insertions, 18 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index eb4e5ae7d3..8c55a57051 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -136,7 +136,7 @@ type 'a gen_atomic_tactic_expr =
   | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-      (clear_flag * 'nam * 'dtrm intro_pattern_expr located option) option
+      ('nam * 'dtrm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacFix of Id.t option * int
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c94ac846f1..8e5e1f1fb8 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -399,7 +399,7 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   in_hyp_as:
-    [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (None,id,ipat)
+    [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
       | -> None ] ]
   ;
   orient:
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a669aef9a8..bc559460e0 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -581,8 +581,7 @@ module Make
 
   let pr_in_hyp_as prc pr_id = function
     | None -> mt ()
-    | Some (clear,id,ipat) ->
-      pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat
+    | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
 
   let pr_clauses default_is_concl pr_id = function
     | { onhyps=Some []; concl_occs=occs }
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index fb22da83aa..1778221b02 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -400,8 +400,8 @@ let intern_red_expr ist = function
   | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
 
-let intern_in_hyp_as ist lf (clear,id,ipat) =
-  (clear,intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
+let intern_in_hyp_as ist lf (id,ipat) =
+  (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
 
 let intern_hyp_list ist = List.map (intern_hyp ist)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ee21a51598..693b382cac 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -902,9 +902,9 @@ let interp_intro_pattern_option ist env sigma = function
       let sigma, ipat = interp_intro_pattern ist env sigma ipat in
       sigma, Some ipat
 
-let interp_in_hyp_as ist env sigma (clear,id,ipat) =
+let interp_in_hyp_as ist env sigma (id,ipat) =
   let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
-  sigma,(clear,interp_hyp ist env sigma id,ipat)
+  sigma,(interp_hyp ist env sigma id,ipat)
 
 let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
@@ -1835,8 +1835,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma,tac = match cl with
           | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
           | Some cl ->
-              let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in
-              sigma, Tactics.apply_delayed_in a ev clear id l cl in
+              let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in
+              sigma, Tactics.apply_delayed_in a ev id l cl in
         Tacticals.New.tclWITHHOLES ev tac sigma
       end
       end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8daa7c4b86..d4480ec922 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2287,7 +2287,7 @@ let assert_as first hd ipat t =
 (* apply in as *)
 
 let general_apply_in sidecond_first with_delta with_destruct with_evars
-    with_clear id lemmas ipat =
+    id lemmas ipat =
   let tac (naming,lemma) tac id =
     apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
       naming id lemma tac in
@@ -2312,12 +2312,12 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
     Tacticals.New.tclTHENFIRST (tclMAPFIRST tac lemmas_target) (ipat_tac id)
 *)
 
-let apply_in simple with_evars clear_flag id lemmas ipat =
+let apply_in simple with_evars id lemmas ipat =
   let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, fun _ sigma -> sigma, l)) lemmas in
-  general_apply_in false simple simple with_evars clear_flag id lemmas ipat
+  general_apply_in false simple simple with_evars id lemmas ipat
 
-let apply_delayed_in simple with_evars clear_flag id lemmas ipat =
-  general_apply_in false simple simple with_evars clear_flag id lemmas ipat
+let apply_delayed_in simple with_evars id lemmas ipat =
+  general_apply_in false simple simple with_evars id lemmas ipat
 
 (*****************************)
 (* Tactics abstracting terms *)
@@ -4553,7 +4553,7 @@ module Simple = struct
   let case   c = general_case_analysis false None (c,NoBindings)
 
   let apply_in id c =
-    apply_in false false None id [None,(Loc.ghost, (c, NoBindings))] None
+    apply_in false false id [None,(Loc.ghost, (c, NoBindings))] None
 
 end
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ade89fc989..b9a0184180 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -196,12 +196,12 @@ val eapply_with_bindings  : constr with_bindings -> unit Proofview.tactic
 val cut_and_apply         : constr -> unit Proofview.tactic
 
 val apply_in :
-  advanced_flag -> evars_flag -> clear_flag -> Id.t -> 
+  advanced_flag -> evars_flag -> Id.t -> 
     (clear_flag * constr with_bindings located) list ->
     intro_pattern option -> unit Proofview.tactic
 
 val apply_delayed_in :
-  advanced_flag -> evars_flag -> clear_flag -> Id.t -> 
+  advanced_flag -> evars_flag -> Id.t -> 
     (clear_flag * delayed_open_constr_with_bindings located) list ->
     intro_pattern option -> unit Proofview.tactic