aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml19
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml6
-rw-r--r--plugins/fourier/fourierR.ml22
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/rtauto/refl_tauto.ml2
5 files changed, 23 insertions, 30 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b85b7995c..2de0fe717 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -249,28 +249,23 @@ let app_global f args k =
let new_app_global f args k =
Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
-let new_exact_check c = Proofview.V82.tactic (exact_check c)
let new_refine c = Proofview.V82.tactic (refine c)
let rec proof_tac p : unit Proofview.tactic =
Proofview.Goal.enter begin fun gl ->
- let type_of = Tacmach.New.pf_type_of gl in
+ let type_of t = Tacmach.New.pf_type_of gl t in
try (* type_of can raise exceptions *)
match p.p_rule with
- Ax c -> new_exact_check c
+ Ax c -> exact_check c
| SymAx c ->
- Proofview.V82.tactic begin fun gls ->
let l=constr_of_term p.p_lhs and
r=constr_of_term p.p_rhs in
- let typ = (* Termops.refresh_universes *)pf_type_of gls l in
- (app_global _sym_eq [|typ;r;l;c|] exact_check) gls
- end
+ let typ = (* Termops.refresh_universes *) type_of l in
+ new_app_global _sym_eq [|typ;r;l;c|] exact_check
| Refl t ->
- Proofview.V82.tactic begin fun gls ->
let lr = constr_of_term t in
- let typ = (* Termops.refresh_universes *) (pf_type_of gls lr) in
- (app_global _refl_equal [|typ;constr_of_term t|] exact_check) gls
- end
+ let typ = (* Termops.refresh_universes *) type_of lr in
+ new_app_global _refl_equal [|typ;constr_of_term t|] exact_check
| Trans (p1,p2)->
let t1 = constr_of_term p1.p_lhs and
t2 = constr_of_term p1.p_rhs and
@@ -339,7 +334,7 @@ let refute_tac c t1 t2 p =
let refine_exact_check c gl =
let evm, _ = pf_apply e_type_of gl c in
- Tacticals.tclTHEN (Refiner.tclEVARS evm) (exact_check c) gl
+ Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
let convert_to_goal_tac c t1 t2 p =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 97989e268..c230a9896 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -437,7 +437,7 @@ let thus_tac c ctyp submetas gls =
with Not_found ->
error "I could not relate this statement to the thesis." in
if List.is_empty list then
- exact_check proof gls
+ Proofview.V82.of_tactic (exact_check proof) gls
else
let refiner = concl_refiner list proof gls in
Tactics.refine refiner gls
@@ -534,14 +534,14 @@ let instr_rew _thus rew_side cut gls0 =
tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
[tclTHEN tcl_erase_info
(tclTHENS (Proofview.V82.of_tactic (transitivity lhs))
- [just_tac;exact_check (mkVar last_id)]);
+ [just_tac;Proofview.V82.of_tactic (exact_check (mkVar last_id))]);
thus_tac new_eq] gls0
| Rhs ->
let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in
tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
[tclTHEN tcl_erase_info
(tclTHENS (Proofview.V82.of_tactic (transitivity rhs))
- [exact_check (mkVar last_id);just_tac]);
+ [Proofview.V82.of_tactic (exact_check (mkVar last_id));just_tac]);
thus_tac new_eq] gls0
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index d34d50364..1f6ece602 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -422,18 +422,16 @@ let my_cut c gl=
let exact = exact_check;;
-let tac_use h = match h.htype with
- "Rlt" -> exact h.hname
- |"Rle" -> exact h.hname
- |"Rgt" -> (tclTHEN (apply (get coq_Rfourier_gt_to_lt))
- (exact h.hname))
- |"Rge" -> (tclTHEN (apply (get coq_Rfourier_ge_to_le))
- (exact h.hname))
- |"eqTLR" -> (tclTHEN (apply (get coq_Rfourier_eqLR_to_le))
- (exact h.hname))
- |"eqTRL" -> (tclTHEN (apply (get coq_Rfourier_eqRL_to_le))
- (exact h.hname))
- |_->assert false
+let tac_use h =
+ let tac = Proofview.V82.of_tactic (exact h.hname) in
+ match h.htype with
+ "Rlt" -> tac
+ |"Rle" -> tac
+ |"Rgt" -> (tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac)
+ |"Rge" -> (tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac)
+ |"eqTLR" -> (tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac)
+ |"eqTRL" -> (tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac)
+ |_->assert false
;;
(*
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2c153becf..20304b529 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -427,7 +427,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
(* replacing [res] with its value *)
observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
(* Conclusion *)
- observe_tac "exact" (fun g -> exact_check (app_constructor g) g)
+ observe_tac "exact" (fun g -> Proofview.V82.of_tactic (exact_check (app_constructor g)) g)
]
)
g
@@ -478,7 +478,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
observe_tac "principle" (Proofview.V82.of_tactic (assert_by
(Name principle_id)
princ_type
- (Proofview.V82.tactic (exact_check f_principle))));
+ (exact_check f_principle)));
observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
observe_tac "idtac" tclIDTAC;
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index bff574a06..6b4be4e2a 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -313,7 +313,7 @@ let rtauto_tac gls=
let tac_start_time = System.get_time () in
let result=
if !check then
- Tactics.exact_check term gls
+ Proofview.V82.of_tactic (Tactics.exact_check term) gls
else
Tactics.exact_no_check term gls in
let tac_end_time = System.get_time () in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 13:49:12 +0000