aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml12
-rw-r--r--tactics/elimschemes.ml34
-rw-r--r--tactics/elimschemes.mli8
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/equality.ml23
-rw-r--r--tactics/hints.ml6
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tactics.ml61
-rw-r--r--tactics/tactics.mli4
9 files changed, 76 insertions, 76 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4bde427b15..5fbf59b815 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -250,7 +250,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
let open Clenv in
let env = Proofview.Goal.env gls in
let concl = Proofview.Goal.concl gls in
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let sigma, term, ty =
if poly then
let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
@@ -649,8 +649,9 @@ module V85 = struct
Goal.V82.hyps gls.Evd.sigma (sig_it gls)
let make_autogoal_hints =
- let cache = ref (true, Environ.empty_named_context_val,
- Hint_db.empty full_transparent_state true)
+ let cache = Summary.ref ~name:"make_autogoal_hints_cache"
+ (true, Environ.empty_named_context_val,
+ Hint_db.empty full_transparent_state true)
in
fun only_classes ?(st=full_transparent_state) g ->
let sign = pf_filtered_hyps g in
@@ -979,8 +980,9 @@ module Search = struct
search_hints : hint_db; }
(** Local hints *)
- let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty,
- Hint_db.empty full_transparent_state true)
+ let autogoal_cache = Summary.ref ~name:"autogoal_cache"
+ (DirPath.empty, true, Context.Named.empty,
+ Hint_db.empty full_transparent_state true)
let make_autogoal_hints only_classes ?(st=full_transparent_state) g =
let open Proofview in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 466b1350d9..99761437eb 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -47,7 +47,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
(nf c', Evd.evar_universe_context sigma), eff
else
let mib,mip = Inductive.lookup_mind_specif env ind in
- let ctx = Declareops.inductive_context mib in
+ let ctx = Declareops.inductive_polymorphic_context mib in
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
let ectx = Evd.evar_universe_context_of ctxset in
@@ -60,7 +60,7 @@ let build_induction_scheme_in_type dep sort ind =
let sigma = Evd.from_env env in
let ctx =
let mib,mip = Inductive.lookup_mind_specif env ind in
- Declareops.inductive_context mib
+ Declareops.inductive_polymorphic_context mib
in
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
@@ -80,30 +80,30 @@ let rect_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
(fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants)
-let ind_scheme_kind_from_type =
- declare_individual_scheme_object "_ind_nodep"
- (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp)
-
-let ind_scheme_kind_from_prop =
- declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
- (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp)
-
-let ind_dep_scheme_kind_from_type =
- declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
- (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp)
+let rec_scheme_kind_from_type =
+ declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
+ (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
let rec_scheme_kind_from_prop =
declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
(optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)
-let rec_scheme_kind_from_type =
- declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
- (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
-
let rec_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
(optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)
+let ind_scheme_kind_from_type =
+ declare_individual_scheme_object "_ind_nodep"
+ (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp)
+
+let ind_dep_scheme_kind_from_type =
+ declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
+ (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp)
+
+let ind_scheme_kind_from_prop =
+ declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
+ (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp)
+
(* Case analysis *)
let build_case_analysis_scheme_in_type dep sort ind =
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 77f927f2df..da432beadc 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -10,6 +10,14 @@ open Ind_tables
(** Induction/recursion schemes *)
+val optimize_non_type_induction_scheme :
+ 'a Ind_tables.scheme_kind ->
+ Indrec.dep_flag ->
+ Term.sorts_family ->
+ 'b ->
+ Names.inductive ->
+ (Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants
+
val rect_scheme_kind_from_prop : individual scheme_kind
val ind_scheme_kind_from_prop : individual scheme_kind
val rec_scheme_kind_from_prop : individual scheme_kind
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 0cee4b6edb..10bc6e3e24 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -72,7 +72,7 @@ let generalize_right mk typ c1 c2 =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let store = Proofview.Goal.extra gl in
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in
let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 05c5cd5ec1..6e56dc48e5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -50,13 +50,12 @@ module NamedDecl = Context.Named.Declaration
let discriminate_introduction = ref true
-let discr_do_intro () =
- !discriminate_introduction && Flags.version_strictly_greater Flags.V8_2
+let discr_do_intro () = !discriminate_introduction
open Goptions
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "automatic introduction of hypotheses by discriminate";
optkey = ["Discriminate";"Introduction"];
optread = (fun () -> !discriminate_introduction);
@@ -64,13 +63,11 @@ let _ =
let injection_pattern_l2r_order = ref true
-let use_injection_pattern_l2r_order () =
- !injection_pattern_l2r_order
- && Flags.version_strictly_greater Flags.V8_4
+let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "injection left-to-right pattern order and clear by default when with introduction pattern";
optkey = ["Injection";"L2R";"Pattern";"Order"];
optread = (fun () -> !injection_pattern_l2r_order) ;
@@ -356,7 +353,6 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
if (is_global Coqlib.glob_eq hdcncl ||
(is_global Coqlib.glob_jmeq hdcncl &&
jmeq_same_dom gl ot)) && not dep
- || Flags.version_less_or_equal Flags.V8_2
then
let c =
match EConstr.kind sigma hdcncl with
@@ -1418,7 +1414,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
"" else
" You can try to use option Set Keep Proof Equalities." in
tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
- | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
+ | Inr [([],_,_)] ->
tclZEROMSG (str"Nothing to inject.")
| Inr posns ->
inject_at_positions env sigma l2r u eq_clause posns
@@ -1769,13 +1765,10 @@ type subst_tactic_flags = {
rewrite_dependent_proof : bool
}
-let default_subst_tactic_flags () =
- if Flags.version_strictly_greater Flags.V8_2 then
- { only_leibniz = false; rewrite_dependent_proof = true }
- else
- { only_leibniz = true; rewrite_dependent_proof = false }
+let default_subst_tactic_flags =
+ { only_leibniz = false; rewrite_dependent_proof = true }
-let subst_all ?(flags=default_subst_tactic_flags ()) () =
+let subst_all ?(flags=default_subst_tactic_flags) () =
if !regular_subst_tactic then
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 773abb9f0c..2fc8baa895 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -29,7 +29,6 @@ open Decl_kinds
open Pattern
open Patternops
open Clenv
-open Pfedit
open Tacred
open Printer
open Vernacexpr
@@ -1307,7 +1306,8 @@ let interp_hints poly =
List.init (nconstructors ind)
(fun i -> let c = (ind,i+1) in
let gr = ConstructRef c in
- empty_hint_info, mib.Declarations.mind_polymorphic, true,
+ empty_hint_info,
+ (Declareops.inductive_is_polymorphic mib), true,
PathHints [gr], IsGlobRef gr)
in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
| HintsExtern (pri, patcom, tacexp) ->
@@ -1462,7 +1462,7 @@ let pr_hint_term sigma cl =
(* print all hints that apply to the concl of the current goal *)
let pr_applicable_hint () =
- let pts = get_pftreestate () in
+ let pts = Proof_global.give_me_the_proof () in
let glss = Proof.V82.subgoals pts in
match glss.Evd.it with
| [] -> CErrors.user_err Pp.(str "No focused goal.")
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ec038f638e..2bc9d9f788 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -460,7 +460,7 @@ let raw_inversion inv_kind id status names =
in
let refined id =
let prf = mkApp (mkVar id, args) in
- Refine.refine (fun h -> (h, prf))
+ Refine.refine ~typecheck:false (fun h -> (h, prf))
in
let neqns = List.length realargs in
let as_mode = names != None in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b553f316c2..689cc48aa2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -25,7 +25,6 @@ open Inductiveops
open Reductionops
open Globnames
open Evd
-open Pfedit
open Tacred
open Genredexpr
open Tacmach.New
@@ -64,11 +63,10 @@ let dependent_propositions_elimination = ref true
let use_dependent_propositions_elimination () =
!dependent_propositions_elimination
- && Flags.version_strictly_greater Flags.V8_2
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "dependent-propositions-elimination tactic";
optkey = ["Dependent";"Propositions";"Elimination"];
optread = (fun () -> !dependent_propositions_elimination) ;
@@ -142,11 +140,10 @@ let bracketing_last_or_and_intro_pattern = ref true
let use_bracketing_last_or_and_intro_pattern () =
!bracketing_last_or_and_intro_pattern
- && Flags.version_strictly_greater Flags.V8_4
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "bracketing last or-and introduction pattern";
optkey = ["Bracketing";"Last";"Introduction";"Pattern"];
optread = (fun () -> !bracketing_last_or_and_intro_pattern);
@@ -163,7 +160,7 @@ let _ =
(** This tactic creates a partial proof realizing the introduction rule, but
does not check anything. *)
let unsafe_intro env store decl b =
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let ctx = named_context_val env in
let nctx = push_named_context_val decl ctx in
let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
@@ -200,7 +197,7 @@ let convert_concl ?(check=true) ty k =
let env = Proofview.Goal.env gl in
let store = Proofview.Goal.extra gl in
let conclty = Proofview.Goal.concl gl in
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let sigma =
if check then begin
ignore (Typing.unsafe_type_of env sigma ty);
@@ -222,7 +219,7 @@ let convert_hyp ?(check=true) d =
let store = Proofview.Goal.extra gl in
let sign = convert_hyp check (named_context_val env) sigma d in
let env = reset_with_named_context sign env in
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ~store ty
end
end
@@ -293,7 +290,7 @@ let clear_gen fail = function
in
let env = reset_with_named_context hyps env in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
- (Refine.refine ~unsafe:true begin fun sigma ->
+ (Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true concl
end)
end
@@ -323,7 +320,7 @@ let move_hyp id dest =
let sign = named_context_val env in
let sign' = move_hyp_in_named_context sigma id dest sign in
let env = reset_with_named_context sign' env in
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ~store ty
end
end
@@ -377,7 +374,7 @@ let rename_hyp repl =
let nconcl = subst concl in
let nctx = val_of_named_context nhyps in
let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
end
end
@@ -527,7 +524,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
in
let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
- Refine.refine begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let (sigma, evs) = mk_holes nenv sigma (List.map pi3 all) in
let ids = List.map pi1 all in
let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
@@ -543,7 +540,7 @@ end
let fix ido n = match ido with
| None ->
Proofview.Goal.enter begin fun gl ->
- let name = Pfedit.get_current_proof_name () in
+ let name = Proof_global.get_current_proof_name () in
let id = new_fresh_id [] name gl in
mutual_fix id n [] 0
end
@@ -579,7 +576,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl ->
mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
in
let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
- Refine.refine begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let (ids, types) = List.split all in
let (sigma, evs) = mk_holes nenv sigma types in
let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
@@ -594,7 +591,7 @@ end
let cofix ido = match ido with
| None ->
Proofview.Goal.enter begin fun gl ->
- let name = Pfedit.get_current_proof_name () in
+ let name = Proof_global.get_current_proof_name () in
let id = new_fresh_id [] name gl in
mutual_cofix id [] 0
end
@@ -1140,7 +1137,7 @@ let rec intros_move = function
let tactic_infer_flags with_evar = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = true;
- Pretyping.use_hook = solve_by_implicit_tactic ();
+ Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true }
@@ -1225,7 +1222,7 @@ let cut c =
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
(** Backward compat: normalize [c]. *)
let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
- Refine.refine ~unsafe:true begin fun h ->
+ Refine.refine ~typecheck:false begin fun h ->
let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
let (h, x) = Evarutil.new_evar env h c in
let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
@@ -1666,7 +1663,7 @@ let solve_remaining_apply_goals =
if Typeclasses.is_class_type evd concl then
let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd')
- (Refine.refine ~unsafe:true (fun h -> (h,c')))
+ (Refine.refine ~typecheck:false (fun h -> (h,c')))
else Proofview.tclUNIT ()
with Not_found -> Proofview.tclUNIT ()
else Proofview.tclUNIT ()
@@ -1914,7 +1911,7 @@ let cut_and_apply c =
| Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 ->
let concl = Proofview.Goal.concl gl in
let env = Tacmach.New.pf_env gl in
- Refine.refine begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let typ = mkProd (Anonymous, c2, concl) in
let (sigma, f) = Evarutil.new_evar env sigma typ in
let (sigma, x) = Evarutil.new_evar env sigma c1 in
@@ -1934,7 +1931,7 @@ let cut_and_apply c =
(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
let exact_no_check c =
- Refine.refine ~unsafe:true (fun h -> (h,c))
+ Refine.refine ~typecheck:false (fun h -> (h,c))
let exact_check c =
Proofview.Goal.enter begin fun gl ->
@@ -1959,7 +1956,7 @@ let native_cast_no_check c = cast_no_check Term.NATIVEcast c
let exact_proof c =
let open Tacmach.New in
Proofview.Goal.enter begin fun gl ->
- Refine.refine begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in
let c = EConstr.of_constr c in
let sigma = Evd.merge_universe_context sigma ctx in
@@ -2076,7 +2073,7 @@ let clear_body ids =
Tacticals.New.tclZEROMSG msg
in
check <*>
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true concl
end
end
@@ -2128,7 +2125,7 @@ let apply_type newcl args =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let store = Proofview.Goal.extra gl in
- Refine.refine begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let newcl = nf_betaiota sigma newcl (* As in former Logic.refine *) in
let (sigma, ev) =
Evarutil.new_evar env sigma ~principal:true ~store newcl in
@@ -2149,7 +2146,7 @@ let bring_hyps hyps =
let concl = Tacmach.New.pf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
- Refine.refine begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let (sigma, ev) =
Evarutil.new_evar env sigma ~principal:true ~store newcl in
(sigma, mkApp (ev, args))
@@ -2888,7 +2885,7 @@ let new_generalize_gen_let lconstr =
0 lconstr (concl, sigma, [])
in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Refine.refine begin fun sigma ->
+ (Refine.refine ~typecheck:false begin fun sigma ->
let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true newcl in
(sigma, applist (ev, args))
end)
@@ -3598,7 +3595,7 @@ let mk_term_eq homogeneous env sigma ty t ty' t' =
let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
let open Context.Rel.Declaration in
- Refine.refine begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let eqslen = List.length eqs in
(* Abstract by the "generalized" hypothesis equality proof if necessary. *)
let sigma, abshypeq, abshypt =
@@ -4418,7 +4415,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
(* and destruct has side conditions first *)
Tacticals.New.tclTHENLAST)
(Tacticals.New.tclTHENLIST [
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
let b = not with_evars && with_eq != None in
let (sigma, c) = use_bindings env sigma elim b (c0,lbind) t0 in
let t = Retyping.get_type_of env sigma c in
@@ -4441,7 +4438,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
let env = reset_with_named_context sign env in
let tac =
Tacticals.New.tclTHENLIST [
- Refine.refine ~unsafe:true begin fun sigma ->
+ Refine.refine ~typecheck:false begin fun sigma ->
mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
end;
tac
@@ -5032,11 +5029,11 @@ let name_op_to_name name_op object_kind suffix =
let default_gk = (Global, false, object_kind) in
match name_op with
| Some s ->
- (try let _, gk, _ = current_proof_statement () in s, gk
+ (try let _, gk, _ = Pfedit.current_proof_statement () in s, gk
with NoCurrentProof -> s, default_gk)
| None ->
let name, gk =
- try let name, gk, _ = current_proof_statement () in name, gk
+ try let name, gk, _ = Pfedit.current_proof_statement () in name, gk
with NoCurrentProof -> anon_id, default_gk in
add_suffix name suffix, gk
@@ -5101,7 +5098,7 @@ module New = struct
rZeta=false;rDelta=false;rConst=[]})
{onhyps; concl_occs=AllOccurrences }
- let refine ?unsafe c =
- Refine.refine ?unsafe c <*>
+ let refine ~typecheck c =
+ Refine.refine ~typecheck c <*>
reduce_after_refine
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ec8fe11456..2e17b8dd5c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -435,8 +435,8 @@ end
module New : sig
- val refine : ?unsafe:bool -> (evar_map -> evar_map * constr) -> unit Proofview.tactic
- (** [refine ?unsafe c] is [Refine.refine ?unsafe c]
+ val refine : typecheck:bool -> (evar_map -> evar_map * constr) -> unit Proofview.tactic
+ (** [refine ~typecheck c] is [Refine.refine ~typecheck c]
followed by beta-iota-reduction of the conclusion. *)
val reduce_after_refine : unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 12:56:32 +0000