aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ltac/coretactics.ml42
-rw-r--r--ltac/tacinterp.ml2
-rw-r--r--plugins/firstorder/rules.ml4
-rw-r--r--plugins/rtauto/refl_tauto.ml2
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/elim.ml2
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/tactics.ml17
-rw-r--r--tactics/tactics.mli2
10 files changed, 17 insertions, 20 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 98b77ab35..3849a8440 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -39,7 +39,7 @@ TACTIC EXTEND cut
END
TACTIC EXTEND exact_no_check
- [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ]
+ [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
END
TACTIC EXTEND vm_cast_no_check
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 5e0153fce..7acdff9ac 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1659,7 +1659,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let (sigma, c_interp) = pf_interp_casted_constr ist gl c in
- Sigma.Unsafe.of_pair (Proofview.V82.tactic (Tactics.exact_no_check c_interp), sigma)
+ Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma)
end }
end
| TacApply (a,ev,cb,cl) ->
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index f19cdd2cc..d05e9484a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -58,7 +58,7 @@ let clear_global=function
(* connection rules *)
let axiom_tac t seq=
- try pf_constr_of_global (find_left t seq) exact_no_check
+ try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
with Not_found->tclFAIL 0 (Pp.str "No axiom link")
let ll_atom_tac a backtrack id continue seq=
@@ -151,7 +151,7 @@ let ll_arrow_tac a b c backtrack id continue seq=
clear_global id;
wrap 1 false continue seq];
tclTHENS (Proofview.V82.of_tactic (cut cc))
- [pf_constr_of_global id exact_no_check;
+ [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
tclTHENLIST
[pf_constr_of_global id (fun idc -> generalize [d idc]);
clear_global id;
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 2f3a3e551..73dc13e72 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -316,7 +316,7 @@ let rtauto_tac gls=
if !check then
Proofview.V82.of_tactic (Tactics.exact_check term) gls
else
- Tactics.exact_no_check term gls in
+ Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in
let tac_end_time = System.get_time () in
let _ =
if !check then msg_info (str "Proof term type-checking is on");
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 485559898..cfbcc4750 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -164,7 +164,7 @@ let e_give_exact flags poly (c,clenv) gl =
else c, gl
in
let t1 = pf_unsafe_type_of gl c in
- tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
+ Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) ->
let clenv', c = connect_hint_clenv poly c clenv gls in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 6bbd9b2e8..f0f408c24 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -33,7 +33,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
let t1 = Tacmach.New.pf_unsafe_type_of gl c in
let t2 = Tacmach.New.pf_concl gl in
if occur_existential t1 || occur_existential t2 then
- Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c))
+ Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
else exact_check c
end }
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 33eb80c28..d59c2fba4 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -84,7 +84,7 @@ let general_decompose recognizer c =
(onLastHypId
(ifOnHyp recognizer (general_decompose_aux recognizer)
(fun id -> clear [id])));
- Proofview.V82.tactic (exact_no_check c) ]
+ exact_no_check c ]
end }
let head_in indl t gl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index eecc2b787..572d4b7ab 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1582,7 +1582,7 @@ let substClause l2r c cls =
Proofview.Goal.enter { enter = begin fun gl ->
let eq = pf_apply get_type_of gl c in
tclTHENS (cutSubstClause l2r eq cls)
- [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)]
+ [Proofview.tclUNIT (); exact_no_check c]
end }
let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 01af30049..6bf5831f7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1833,7 +1833,7 @@ let cut_and_apply c =
(* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *)
(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
-let new_exact_no_check c =
+let exact_no_check c =
Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
let exact_check c =
@@ -1845,13 +1845,11 @@ let exact_check c =
let sigma = Sigma.to_evar_map sigma in
let sigma, ct = Typing.type_of env sigma c in
let tac =
- Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c)
+ Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c)
in
Sigma.Unsafe.of_pair (tac, sigma)
end }
-let exact_no_check = Tacmach.refine_no_check
-
let vm_cast_no_check c gl =
let concl = Tacmach.pf_concl gl in
Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl
@@ -2626,8 +2624,7 @@ let forward b usetac ipat c =
Proofview.Goal.enter { enter = begin fun gl ->
let t = Tacmach.New.pf_unsafe_type_of gl c in
let hd = head_ident c in
- Tacticals.New.tclTHENFIRST (assert_as true hd ipat t)
- (Proofview.V82.tactic (exact_no_check c))
+ Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
end }
| Some tac ->
if b then
@@ -2820,14 +2817,14 @@ let specialize (c,lbind) =
(Proofview.Unsafe.tclEVARS sigma)
(Tacticals.New.tclTHENFIRST
(assert_before_replacing id typ)
- (new_exact_no_check term))
+ (exact_no_check term))
| _ ->
(* To deprecate in favor of generalize? *)
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS sigma)
(Tacticals.New.tclTHENLAST
(cut typ)
- (new_exact_no_check term))
+ (exact_no_check term))
end }
(*****************************)
@@ -3652,7 +3649,7 @@ let specialize_eqs id gl =
let ty' = Evarutil.nf_evar !evars ty' in
if worked then
tclTHENFIRST (Tacmach.internal_cut true id ty')
- (exact_no_check ((* refresh_universes_strict *) acc')) gl
+ (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
@@ -4798,7 +4795,7 @@ let abstract_subproof id gk tac =
Entries.(snd (Future.force const.const_entry_body)) in
let solve =
Proofview.tclEFFECTS effs <*>
- new_exact_no_check (applist (lem, args))
+ exact_no_check (applist (lem, args))
in
let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
Sigma.Unsafe.of_pair (tac, evd)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 47ff197a0..2ffedf81a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -114,7 +114,7 @@ val intros_patterns : intro_patterns -> unit Proofview.tactic
(** {6 Exact tactics. } *)
val assumption : unit Proofview.tactic
-val exact_no_check : constr -> tactic
+val exact_no_check : constr -> unit Proofview.tactic
val vm_cast_no_check : constr -> tactic
val native_cast_no_check : constr -> tactic
val exact_check : constr -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 07:22:22 +0000