aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ltac/coretactics.ml42
-rw-r--r--ltac/tauto.ml2
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml16
-rw-r--r--plugins/firstorder/rules.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml5
-rw-r--r--plugins/funind/invfun.ml1
-rw-r--r--plugins/funind/recdef.ml14
-rw-r--r--plugins/omega/coq_omega.ml28
-rw-r--r--printing/printer.ml3
-rw-r--r--proofs/logic.ml10
-rw-r--r--proofs/proof_type.mli1
-rw-r--r--proofs/tacmach.ml5
-rw-r--r--proofs/tacmach.mli2
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/elim.ml4
-rw-r--r--tactics/eqdecide.ml1
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tactics.ml96
-rw-r--r--tactics/tactics.mli3
-rw-r--r--toplevel/vernacentries.ml2
21 files changed, 100 insertions, 105 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 8b5f527cd..4e2dfafb5 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -247,7 +247,7 @@ END
TACTIC EXTEND clear
[ "clear" hyp_list(ids) ] -> [
if List.is_empty ids then Tactics.keep []
- else Proofview.V82.tactic (Tactics.clear ids)
+ else Tactics.clear ids
]
| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
END
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index 655bfd5f5..c0cae84c0 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -102,7 +102,7 @@ let assert_ ?by c =
let apply c = Tactics.apply c
-let clear id = Proofview.V82.tactic (fun gl -> Tactics.clear [id] gl)
+let clear id = Tactics.clear [id]
let assumption = Tactics.assumption
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 090b293f5..4f2270313 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -34,6 +34,22 @@ open Context.Named.Declaration
(* Strictness option *)
+let clear ids { it = goal; sigma } =
+ let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
+ let env = Goal.V82.env sigma goal in
+ let sign = Goal.V82.hyps sigma goal in
+ let cl = Goal.V82.concl sigma goal in
+ let evdref = ref (Evd.clear_metas sigma) in
+ let (hyps, concl) =
+ try Evarutil.clear_hyps_in_evi env evdref sign cl ids
+ with Evarutil.ClearDependencyError (id, _) ->
+ errorlabstrm "" (str "Cannot clear " ++ pr_id id)
+ in
+ let sigma = !evdref in
+ let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+ let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
+ { it = [gl]; sigma }
+
let get_its_info gls = get_info gls.sigma gls.it
let get_strictness,set_strictness =
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index c05015c53..f19cdd2cc 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -52,7 +52,7 @@ let basename_of_global=function
| _->assert false
let clear_global=function
- VarRef id->clear [id]
+ VarRef id-> Proofview.V82.of_tactic (clear [id])
| _->tclIDTAC
(* connection rules *)
@@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq=
(fun gls->
let id0=pf_nth_hyp_id gls 1 in
let term=mkApp(idc,[|mkVar(id0)|]) in
- tclTHEN (generalize [term]) (clear [id0]) gls));
+ tclTHEN (generalize [term]) (Proofview.V82.of_tactic (clear [id0])) gls));
clear_global id;
Proofview.V82.of_tactic intro;
tclCOMPLETE (wrap 1 false continue (deepen seq))];
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 839586528..fdb112ba0 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -127,8 +127,7 @@ let finish_proof dynamic_infos g =
let refine c =
Tacmach.refine c
-let thin l =
- Tacmach.thin_no_check l
+let thin l = Proofview.V82.of_tactic (Tactics.clear l)
let eq_constr u v = eq_constr_nounivs u v
@@ -1565,7 +1564,7 @@ let prove_principle_for_gen
Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
in
let revert l =
- tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l)
+ tclTHEN (Tactics.generalize (List.map mkVar l)) (Proofview.V82.of_tactic (clear l))
in
let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
let prove_rec_arg_acc g =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 6a5a5ad53..fde1b7e70 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -94,6 +94,7 @@ let nf_zeta =
Environ.empty_env
Evd.empty
+let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
(* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *)
(* let id_to_constr id = *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e98ac5fb5..ac81366bb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -267,8 +267,8 @@ let observe_tclTHENLIST s tacl =
let tclUSER tac is_mes l g =
let clear_tac =
match l with
- | None -> clear []
- | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l)
+ | None -> tclIDTAC
+ | Some l -> tclMAP (fun id -> tclTRY (Proofview.V82.of_tactic (clear [id]))) (List.rev l)
in
observe_tclTHENLIST (str "tclUSER1")
[
@@ -399,7 +399,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
Proofview.V82.of_tactic (intro_using teq_id);
onLastHypId (fun heq ->
observe_tclTHENLIST (str "treat_case2")[
- thin to_intros;
+ Proofview.V82.of_tactic (clear to_intros);
h_intros to_intros;
(fun g' ->
let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
@@ -560,7 +560,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
Proofview.V82.of_tactic default_full_auto];
observe_tclTHENLIST (str "destruct_bounds_aux2")[
- observe_tac (str "clearing k ") (clear [id]);
+ observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id]));
h_intros [k;h';def];
observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl));
observe_tac (str "unfold functional")
@@ -589,7 +589,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
| (_,v_bound)::l ->
observe_tclTHENLIST (str "destruct_bounds_aux3")[
Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
- clear [v_bound];
+ Proofview.V82.of_tactic (clear [v_bound]);
tclDO 2 (Proofview.V82.of_tactic intro);
onNthHypId 1
(fun p_hyp ->
@@ -948,7 +948,7 @@ let rec destruct_hex expr_info acc l =
| (v,hex)::l ->
observe_tclTHENLIST (str "destruct_hex")[
Proofview.V82.of_tactic (simplest_case (mkVar hex));
- clear [hex];
+ Proofview.V82.of_tactic (clear [hex]);
tclDO 2 (Proofview.V82.of_tactic intro);
onNthHypId 1 (fun hp ->
onNthHypId 2 (fun p ->
@@ -1116,7 +1116,7 @@ let termination_proof_header is_mes input_type ids args_id relation
[observe_tac (str "generalize")
(onNLastHypsId (nargs+1)
(tclMAP (fun id ->
- tclTHEN (Tactics.generalize [mkVar id]) (clear [id]))
+ tclTHEN (Tactics.generalize [mkVar id]) (Proofview.V82.of_tactic (clear [id])))
))
;
observe_tac (str "fix") (fix (Some hrec) (nargs+1));
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 1f420cf6a..fc5054080 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1122,7 +1122,7 @@ let replay_history tactic_normalisation =
Proofview.V82.tactic (generalize_tac
[mkApp (Lazy.force coq_OMEGA1,
[| eq1; rhs; mkVar aux; mkVar id |])]);
- Proofview.V82.tactic (clear [aux;id]);
+ (clear [aux;id]);
(intros_using [id]);
(cut (mk_gt kk dd)) ])
[ Tacticals.New.tclTHENS
@@ -1132,7 +1132,7 @@ let replay_history tactic_normalisation =
(Proofview.V82.tactic (generalize_tac
[mkApp (Lazy.force coq_Zmult_le_approx,
[| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]));
- Proofview.V82.tactic (clear [aux1;aux2;id]);
+ (clear [aux1;aux2;id]);
(intros_using [id]);
(loop l) ];
Tacticals.New.tclTHENLIST [
@@ -1160,7 +1160,7 @@ let replay_history tactic_normalisation =
Proofview.V82.tactic (generalize_tac
[mkApp (Lazy.force coq_OMEGA4,
[| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
- Proofview.V82.tactic (clear [aux1;aux2]);
+ (clear [aux1;aux2]);
unfold sp_not;
(intros_using [aux]);
Proofview.V82.tactic (resolve_id aux);
@@ -1190,7 +1190,7 @@ let replay_history tactic_normalisation =
Proofview.V82.tactic (generalize_tac
[mkApp (Lazy.force coq_OMEGA18,
[| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
- Proofview.V82.tactic (clear [aux1;id]);
+ (clear [aux1;id]);
(intros_using [id]);
(loop l) ];
Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
@@ -1205,7 +1205,7 @@ let replay_history tactic_normalisation =
Proofview.V82.tactic (generalize_tac
[mkApp (Lazy.force coq_OMEGA3,
[| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
- Proofview.V82.tactic (clear [aux1;aux2;id]);
+ (clear [aux1;aux2;id]);
(intros_using [id]);
(loop l) ];
Tacticals.New.tclTHENLIST [
@@ -1231,7 +1231,7 @@ let replay_history tactic_normalisation =
(intros_using [aux]);
Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
[| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
- Proofview.V82.tactic (clear [id1;id2;aux]);
+ (clear [id1;id2;aux]);
(intros_using [id]);
(loop l) ];
Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity]
@@ -1263,13 +1263,13 @@ let replay_history tactic_normalisation =
[Tacticals.New.tclTHENLIST [
(intros_using [aux]);
(elim_id aux);
- Proofview.V82.tactic (clear [aux]);
+ (clear [aux]);
(intros_using [vid; aux]);
Proofview.V82.tactic (generalize_tac
[mkApp (Lazy.force coq_OMEGA9,
[| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
Proofview.V82.tactic (mk_then tac);
- Proofview.V82.tactic (clear [aux]);
+ (clear [aux]);
(intros_using [id]);
(loop l) ];
Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ]
@@ -1325,7 +1325,7 @@ let replay_history tactic_normalisation =
eq1;eq2;kk1;kk2;
mkVar aux1;mkVar aux2;
mkVar id1;mkVar id2 |])]);
- Proofview.V82.tactic (clear [aux1;aux2]);
+ (clear [aux1;aux2]);
Proofview.V82.tactic (mk_then tac);
(intros_using [id]);
(loop l) ];
@@ -1367,7 +1367,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
let shift_left =
tclTHEN
(generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
- (tclTRY (clear [id]))
+ (tclTRY (Proofview.V82.of_tactic (clear [id])))
in
if not (List.is_empty tac) then
let id' = new_identifier () in
@@ -1412,7 +1412,7 @@ let destructure_omega gl tac_def (id,c) =
let reintroduce id =
(* [id] cannot be cleared if dependent: protect it by a try *)
- Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) (intro_using id)
+ Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) (intro_using id)
open Proofview.Notations
@@ -1435,7 +1435,7 @@ let coq_omega =
(simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
(intros_using [v; id]);
(elim_id id);
- Proofview.V82.tactic (clear [id]);
+ (clear [id]);
(intros_using [th;id]);
tac ]),
{kind = INEQ;
@@ -1674,7 +1674,7 @@ let onClearedName id tac =
(* We cannot ensure that hyps can be cleared (because of dependencies), *)
(* so renaming may be necessary *)
Tacticals.New.tclTHEN
- (Proofview.V82.tactic (tclTRY (clear [id])))
+ (Tacticals.New.tclTRY (clear [id]))
(Proofview.Goal.nf_enter { enter = begin fun gl ->
let id = Tacmach.New.of_old (fresh_id [] id) gl in
Tacticals.New.tclTHEN (introduction id) (tac id)
@@ -1682,7 +1682,7 @@ let onClearedName id tac =
let onClearedName2 id tac =
Tacticals.New.tclTHEN
- (Proofview.V82.tactic (tclTRY (clear [id])))
+ (Tacticals.New.tclTRY (clear [id]))
(Proofview.Goal.nf_enter { enter = begin fun gl ->
let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
diff --git a/printing/printer.ml b/printing/printer.ml
index a16a92d0a..401f5f99e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -711,9 +711,6 @@ let pr_prim_rule = function
str(if Termops.occur_meta c then "refine " else "exact ") ++
Constrextern.with_meta_as_hole pr_constr c
- | Thin ids ->
- (str"clear " ++ pr_sequence pr_id ids)
-
| Move (id1,id2) ->
(str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 09f308abe..df5a12473 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -636,16 +636,6 @@ let prim_refiner r sigma goal =
let sigma = Goal.V82.partial_solution sigma goal oterm in
(sgl, sigma)
- (* And now the structural rules *)
- | Thin ids ->
- let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
- let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in
- let (gl,ev,sigma) =
- Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)
- in
- let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
- ([gl], sigma)
-
| Move (hfrom, hto) ->
let (left,right,declfrom,toleft) =
split_sign hfrom hto (named_context_of_val sign) in
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index b4c9dae2a..48ad50c7a 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -22,7 +22,6 @@ type prim_rule =
| FixRule of Id.t * int * (Id.t * int * constr) list * int
| Cofix of Id.t * (Id.t * constr) list * int
| Refine of constr
- | Thin of Id.t list
| Move of Id.t * Id.t move_location
(** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 33cef7486..67daccb81 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -121,10 +121,6 @@ let internal_cut_rev_no_check replace id t gl =
let refine_no_check c gl =
refiner (Refine c) gl
-(* This does not check dependencies *)
-let thin_no_check ids gl =
- if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl
-
let move_hyp_no_check id1 id2 gl =
refiner (Move (id1,id2)) gl
@@ -139,7 +135,6 @@ let mutual_cofix f others j gl =
let internal_cut b d t = with_check (internal_cut_no_check b d t)
let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
let refine c = with_check (refine_no_check c)
-let thin c = with_check (thin_no_check c)
let move_hyp id id' = with_check (move_hyp_no_check id id')
(* Pretty-printers *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f786b5f21..fef205f82 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -86,7 +86,6 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
val refiner : rule -> tactic
val internal_cut_no_check : bool -> Id.t -> types -> tactic
val refine_no_check : constr -> tactic
-val thin_no_check : Id.t list -> tactic
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic
@@ -96,7 +95,6 @@ val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic
val internal_cut : bool -> Id.t -> types -> tactic
val internal_cut_rev : bool -> Id.t -> types -> tactic
val refine : constr -> tactic
-val thin : Id.t list -> tactic
val move_hyp : Id.t -> Id.t move_location -> tactic
(** {6 Pretty-printing functions (debug only). } *)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 6d6e51536..9ae0ab90b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -151,7 +151,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
begin
let gl'' =
if !to_be_cleared then
- tclTHEN (fun _ -> gl') (tclTRY (clear [!id])) gl
+ tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl
else gl' in
id := lastid ;
to_be_cleared := true ;
diff --git a/tactics/elim.ml b/tactics/elim.ml
index d441074f6..33eb80c28 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -63,7 +63,7 @@ and general_decompose_aux recognizer id =
elimHypThen
(introElimAssumsThen
(fun bas ->
- tclTHEN (Proofview.V82.tactic (clear [id]))
+ tclTHEN (clear [id])
(tclMAP (general_decompose_on_hyp recognizer)
(ids_of_named_context bas.Tacticals.assums))))
id
@@ -83,7 +83,7 @@ let general_decompose recognizer c =
[ tclTHEN (intro_using tmphyp_name)
(onLastHypId
(ifOnHyp recognizer (general_decompose_aux recognizer)
- (fun id -> Proofview.V82.tactic (clear [id]))));
+ (fun id -> clear [id])));
Proofview.V82.tactic (exact_no_check c) ]
end }
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index ef361d326..01ebaa7b7 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -49,7 +49,6 @@ open Coqlib
Eduardo Gimenez (30/3/98).
*)
-let clear ids = Proofview.V82.tactic (clear ids)
let clear_last = (onLastHyp (fun c -> (clear [destVar c])))
let choose_eq eqonleft =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index cb1d82ae6..eecc2b787 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -79,8 +79,6 @@ let _ =
(* Rewriting tactics *)
-let clear ids = Proofview.V82.tactic (clear ids)
-
let tclNOTSAMEGOAL tac =
Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac))
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 89c6beb32..3707ef90b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -30,8 +30,6 @@ open Sigma.Notations
open Proofview.Notations
open Context.Named.Declaration
-let clear hyps = Proofview.V82.tactic (clear hyps)
-
let var_occurs_in_pf gl id =
let env = Proofview.Goal.env gl in
occur_var env id (Proofview.Goal.concl gl) ||
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2fe4d620e..b266438f9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -271,25 +271,45 @@ let replacing_dependency_msg env sigma id = function
let error_replacing_dependency env sigma id err =
errorlabstrm "" (replacing_dependency_msg env sigma id err)
-let thin l gl =
- try Tacmach.thin l gl
- with Evarutil.ClearDependencyError (id,err) ->
- error_clear_dependency (pf_env gl) (project gl) id err
+(* This tactic enables the user to remove hypotheses from the signature.
+ * Some care is taken to prevent him from removing variables that are
+ * subsequently used in other hypotheses or in the conclusion of the
+ * goal. *)
-let thin_for_replacing l gl =
- try Tacmach.thin l gl
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency (pf_env gl) (project gl) id err
+let clear_gen fail = function
+| [] -> Proofview.tclUNIT ()
+| ids ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
+ let ids = List.fold_right Id.Set.add ids Id.Set.empty in
+ (** clear_hyps_in_evi does not require nf terms *)
+ let gl = Proofview.Goal.assume gl in
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let concl = Proofview.Goal.concl gl in
+ let evdref = ref sigma in
+ let (hyps, concl) =
+ try clear_hyps_in_evi env evdref (named_context_val env) concl ids
+ with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
+ in
+ let env = reset_with_named_context hyps env in
+ let tac = Refine.refine ~unsafe:true { run = fun sigma ->
+ Evarutil.new_evar env sigma ~principal:true concl
+ } in
+ Sigma.Unsafe.of_pair (tac, !evdref)
+ end }
+
+let clear ids = clear_gen error_clear_dependency ids
+let clear_for_replacing ids = clear_gen error_replacing_dependency ids
let apply_clear_request clear_flag dft c =
let check_isvar c =
if not (isVar c) then
error "keep/clear modifiers apply only to hypothesis names." in
- let clear = match clear_flag with
+ let doclear = match clear_flag with
| None -> dft && isVar c
| Some true -> check_isvar c; true
| Some false -> false in
- if clear then Proofview.V82.tactic (thin [destVar c])
+ if doclear then clear [destVar c]
else Tacticals.New.tclIDTAC
(* Moving hypotheses *)
@@ -890,7 +910,7 @@ let intro_replacing id =
Proofview.Goal.enter { enter = begin fun gl ->
let next_hyp = get_next_hyp_position id gl in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (thin_for_replacing [id]);
+ clear_for_replacing [id];
introduction id;
Proofview.V82.tactic (move_hyp id next_hyp);
]
@@ -910,7 +930,7 @@ let intros_possibly_replacing ids =
let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
Tacticals.New.tclTHEN
(Tacticals.New.tclMAP (fun id ->
- Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id])))
+ Tacticals.New.tclTRY (clear_for_replacing [id]))
(if suboptimal then ids else List.rev ids))
(Tacticals.New.tclMAP (fun (id,pos) ->
Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id))
@@ -922,7 +942,7 @@ let intros_replacing ids =
Proofview.Goal.enter { enter = begin fun gl ->
let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
Tacticals.New.tclTHEN
- (Proofview.V82.tactic (thin_for_replacing ids))
+ (clear_for_replacing ids)
(Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
end }
@@ -1563,7 +1583,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
(fun b id ->
Tacticals.New.tclTHEN
(try_main_apply b (mkVar id))
- (Proofview.V82.tactic (thin [id])))
+ (clear [id]))
(exn0, info) c
else
Proofview.tclZERO ~info exn0 in
@@ -1690,7 +1710,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
(fun id ->
Tacticals.New.tclTHENLIST [
apply_clear_request clear_flag false c;
- Proofview.V82.tactic (thin idstoclear);
+ clear idstoclear;
tac id
])
with e when with_destruct && Errors.noncritical e ->
@@ -1823,14 +1843,6 @@ let assumption =
(* Modification of a local context *)
(*****************************************************************)
-(* This tactic enables the user to remove hypotheses from the signature.
- * Some care is taken to prevent him from removing variables that are
- * subsequently used in other hypotheses or in the conclusion of the
- * goal. *)
-
-let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
- if List.is_empty ids then tclIDTAC else thin ids
-
let on_the_bodies = function
| [] -> assert false
| [id] -> str " depends on the body of " ++ pr_id id
@@ -1912,13 +1924,7 @@ let clear_body ids =
end }
let clear_wildcards ids =
- Proofview.V82.tactic (tclMAP (fun (loc,id) gl ->
- try with_check (Tacmach.thin_no_check [id]) gl
- with ClearDependencyError (id,err) ->
- (* Intercept standard [thin] error message *)
- Loc.raise loc
- (error_clear_dependency (pf_env gl) (project gl) (Id.of_string "_") err))
- ids)
+ Tacticals.New.tclMAP (fun (loc, id) -> clear [id]) ids
(* Takes a list of booleans, and introduces all the variables
* quantified in the goal which are associated with a value
@@ -1929,7 +1935,7 @@ let rec intros_clearing = function
| (false::tl) -> Tacticals.New.tclTHEN intro (intros_clearing tl)
| (true::tl) ->
Tacticals.New.tclTHENLIST
- [ intro; Tacticals.New.onLastHypId (fun id -> Proofview.V82.tactic (clear [id])); intros_clearing tl]
+ [ intro; Tacticals.New.onLastHypId (fun id -> clear [id]); intros_clearing tl]
(* Keeping only a few hypotheses *)
@@ -1948,7 +1954,7 @@ let keep hyps =
else (hyp::clear,keep))
~init:([],[]) (Proofview.Goal.env gl)
in
- Proofview.V82.tactic (fun gl -> thin cl gl)
+ clear cl
end }
(*********************************)
@@ -1995,7 +2001,7 @@ let revert hyps =
Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in
- (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps))
+ (bring_hyps ctx) <*> (clear hyps)
end }
(************************)
@@ -2137,7 +2143,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
let ll = get_and_check_or_and_pattern loc ll branchsigns in
Tacticals.New.tclTHENLASTn
- (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id])))
+ (Tacticals.New.tclTHEN (simplest_case c) (clear [id]))
(Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
nv_with_let ll)
end }
@@ -2164,20 +2170,20 @@ let rewrite_hyp_then assert_style thin l2r id tac =
let id' = destVar rhs in
subst_on l2r id' lhs, early_clear id' thin
else
- Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])),
+ Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]),
thin
| Some (hdcncl,[c]) ->
let l2r = not l2r in (* equality of the form eq_true *)
if isVar c then
let id' = destVar c in
Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl)
- (Proofview.V82.tactic (clear_var_and_eq id')),
+ (clear_var_and_eq id'),
early_clear id' thin
else
- Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])),
+ Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]),
thin
| _ ->
- Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])),
+ Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]),
thin in
(* Skip the side conditions of the rewriting step *)
Tacticals.New.tclTHENFIRST eqtac (tac thin)
@@ -2314,7 +2320,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
if naming = NamingMustBe (loc,id) then
Proofview.tclUNIT () (* apply_in_once do a replacement *)
else
- Proofview.V82.tactic (clear [id]) in
+ clear [id] in
let f = { delayed = fun env sigma ->
let Sigma (c, sigma, p) = f.delayed env sigma in
Sigma ((c, NoBindings), sigma, p)
@@ -2653,7 +2659,7 @@ let generalize_dep ?(with_let=false) c gl =
tclTHENLIST
[tclEVARS evd;
Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
- thin (List.rev tothin')]
+ Proofview.V82.of_tactic (clear (List.rev tothin'))]
gl
(** *)
@@ -2789,7 +2795,7 @@ let unfold_body x =
end }
(* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = Tacticals.New.tclTHEN (Tacticals.New.tclTRY (unfold_body id)) (Proofview.V82.tactic (clear [id]))
+let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
(*****************************)
(* High-level induction *)
@@ -3523,7 +3529,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))]
else Tacticals.New.tclTHENLIST [
tac;
- Proofview.V82.tactic (clear [id]);
+ clear [id];
Tacticals.New.tclDO n intro]
in
if List.is_empty vars then tac
@@ -3590,7 +3596,7 @@ let specialize_eqs id gl =
let specialize_eqs id gl =
if
- (try ignore(clear [id] gl); false
+ (try ignore(Proofview.V82.of_tactic (clear [id]) gl); false
with e when Errors.noncritical e -> true)
then
tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl
@@ -4044,7 +4050,7 @@ let clear_unselected_context id inhyps cls gl =
let test id = occur_var_in_decl (pf_env gl) id d in
if List.exists test (id::inhyps) then Some id' else None in
let ids = List.map_filter to_erase (pf_hyps gl) in
- thin ids gl
+ Proofview.V82.of_tactic (clear ids) gl
| None -> tclIDTAC gl
let use_bindings env sigma elim must_be_closed (c,lbind) typ =
@@ -4148,7 +4154,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
end };
if with_evars then Proofview.shelve_unifiable else guard_no_unifiable;
if is_arg_pure_hyp
- then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0]))
+ then Tacticals.New.tclTRY (clear [destVar c0])
else Proofview.tclUNIT ();
if isrec then Proofview.cycle (-1) else Proofview.tclUNIT ()
])
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 4c4a96ec0..87400bfdf 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -35,7 +35,6 @@ val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic
val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic
-val thin : Id.t list -> tactic
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
val fix : Id.t option -> int -> tactic
@@ -163,7 +162,7 @@ val unfold_constr : global_reference -> unit Proofview.tactic
(** {6 Modification of the local context. } *)
-val clear : Id.t list -> tactic
+val clear : Id.t list -> unit Proofview.tactic
val clear_body : Id.t list -> unit Proofview.tactic
val unfold_body : Id.t -> unit Proofview.tactic
val keep : Id.t list -> unit Proofview.tactic
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b40f61b15..0e5cef828 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -861,7 +861,7 @@ let vernac_set_used_variables e =
Proof_global.with_current_proof begin fun _ p ->
if List.is_empty to_clear then (p, ())
else
- let tac = Proofview.V82.tactic (Tactics.clear to_clear) in
+ let tac = Tactics.clear to_clear in
fst (solve SelectAll None tac p), ()
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 21:53:41 +0000