aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tactics.ml44
-rw-r--r--tactics/tactics.mli4
5 files changed, 27 insertions, 27 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4bde427b1..2faf1e0ec 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
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 0cee4b6ed..10bc6e3e2 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/inv.ml b/tactics/inv.ml
index ec038f638..2bc9d9f78 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 7e560b176..d0c6fdca5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -162,7 +162,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
@@ -199,7 +199,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);
@@ -221,7 +221,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
@@ -292,7 +292,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
@@ -322,7 +322,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
@@ -376,7 +376,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
@@ -526,7 +526,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
@@ -578,7 +578,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
@@ -1224,7 +1224,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
@@ -1665,7 +1665,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 ()
@@ -1913,7 +1913,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
@@ -1933,7 +1933,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 ->
@@ -1958,7 +1958,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
@@ -2075,7 +2075,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
@@ -2127,7 +2127,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
@@ -2148,7 +2148,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))
@@ -2887,7 +2887,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)
@@ -3597,7 +3597,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 =
@@ -4417,7 +4417,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
@@ -4440,7 +4440,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
@@ -5100,7 +5100,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 ec8fe1145..2e17b8dd5 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.39.1) at 2024-06-27 16:32:53 +0000