aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-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
-rw-r--r--tactics/auto.ml13
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/tactics.ml41
-rw-r--r--tactics/tactics.mli6
9 files changed, 56 insertions, 59 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
diff --git a/tactics/auto.ml b/tactics/auto.ml
index bcf5e2947..b9c52144e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1172,11 +1172,12 @@ let exact poly (c,clenv) =
else
let ctx = Evd.evar_universe_context clenv.evd in
ctx, c
- in
- fun gl ->
- tclTHEN (Refiner.tclEVARS (Evd.merge_universe_context (project gl) ctx))
- (exact_check c') gl
-
+ in
+ Proofview.Goal.raw_enter begin fun gl ->
+ let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in
+ Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) (exact_check c')
+ end
+
(* Util *)
let expand_constructor_hints env sigma lems =
@@ -1465,7 +1466,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
match t with
| Res_pf (c,cl) -> Proofview.V82.tactic (unify_resolve_gen poly flags (c,cl))
| ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
- | Give_exact (c, cl) -> Proofview.V82.tactic (exact poly (c, cl))
+ | Give_exact (c, cl) -> exact poly (c, cl)
| Res_pf_THEN_trivial_fail (c,cl) ->
Tacticals.New.tclTHEN
(Proofview.V82.tactic (unify_resolve_gen poly flags (c,cl)))
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 4674bd030..bb7d2f0d2 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -35,7 +35,7 @@ let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_tr
let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
if occur_existential t1 || occur_existential t2 then
tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
- else exact_check c gl
+ else Proofview.V82.of_tactic (exact_check c) gl
let assumption id = e_give_exact (mkVar id)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ba389faa9..23c37fb65 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -129,18 +129,18 @@ let convert_concl = Tacmach.convert_concl
let convert_hyp = Tacmach.convert_hyp
let thin_body = Tacmach.thin_body
-let convert_gen pb x y gl =
- try tclEVARS (pf_apply Evd.conversion gl pb x y) gl
- with Reduction.NotConvertible ->
- tclFAIL_lazy 0 (lazy (str"Not convertible"))
- (* Adding more information in this message, even under the lazy, can result in huge *)
- (* blowups, time and spacewise... (see autos used in DoubleCyclic.) 2.3s against 15s. *)
- (* ++ Printer.pr_constr_env env x ++ *)
- (* str" and " ++ Printer.pr_constr_env env y)) *)
- gl
-
-let convert = convert_gen Reduction.CONV
-let convert_leq = convert_gen Reduction.CUMUL
+let convert_gen pb x y =
+ Proofview.Goal.raw_enter begin fun gl ->
+ try
+ let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in
+ Proofview.V82.tclEVARS sigma
+ with (* Reduction.NotConvertible *) _ ->
+ (** FIXME: Sometimes an anomaly is raised from conversion *)
+ Tacticals.New.tclFAIL 0 (str "Not convertible")
+end
+
+let convert x y = convert_gen Reduction.CONV x y
+let convert_leq x y = convert_gen Reduction.CUMUL x y
let error_clear_dependency env id = function
| Evarutil.OccurHypInSimpleClause None ->
@@ -1194,16 +1194,19 @@ 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 exact_check c gl =
- let concl = (pf_concl gl) in
- let ct = pf_type_of gl c in
- try tclTHEN (convert_leq ct concl) (refine_no_check c) gl
- with _ -> error "Not an exact proof." (*FIXME error handling here not the best *)
-
-let exact_no_check = refine_no_check
let new_exact_no_check c =
Proofview.Refine.refine (fun h -> (h, c))
+let exact_check c =
+ Proofview.Goal.raw_enter begin fun gl ->
+ (** We do not need to normalize the goal because we just check convertibility *)
+ let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+ let ct = Tacmach.New.pf_type_of gl c in
+ Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c)
+ end
+
+let exact_no_check = refine_no_check
+
let vm_cast_no_check c gl =
let concl = pf_concl gl in
refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c1911819b..6574d88c5 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -45,8 +45,8 @@ val fix : Id.t option -> int -> tactic
val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic
val cofix : Id.t option -> tactic
-val convert : constr -> constr -> tactic
-val convert_leq : constr -> constr -> tactic
+val convert : constr -> constr -> unit Proofview.tactic
+val convert_leq : constr -> constr -> unit Proofview.tactic
(** {6 Introduction tactics. } *)
@@ -110,7 +110,7 @@ val intros_pattern_bound :
val assumption : unit Proofview.tactic
val exact_no_check : constr -> tactic
val vm_cast_no_check : constr -> tactic
-val exact_check : constr -> tactic
+val exact_check : constr -> unit Proofview.tactic
val exact_proof : Constrexpr.constr_expr -> tactic
(** {6 Reduction tactics. } *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 11:27:56 +0000