From cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Dec 2015 15:18:42 +0100 Subject: Dead code from August 2014 in apply in. --- intf/tacexpr.mli | 2 +- parsing/g_tactic.ml4 | 2 +- printing/pptactic.ml | 3 +-- tactics/tacintern.ml | 4 ++-- tactics/tacinterp.ml | 8 ++++---- tactics/tactics.ml | 12 ++++++------ tactics/tactics.mli | 4 ++-- 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 -- cgit v1.2.3