Dualize the unsafe flag of refine into typecheck and make it mandatory.

16 files changed, 59 insertions, 61 deletions

diff --git a/API/API.mli b/API/API.mli
index 20a637c1f..5a833d08a 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4100,7 +4100,7 @@ sig
 
   module New :
   sig
-    val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
+    val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
     val reduce_after_refine : unit Proofview.tactic
   end
   module Simple :
@@ -4490,7 +4490,7 @@ end
 
 module Refine :
 sig
-  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic
+  val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic
   val solve_constraints : unit Proofview.tactic
 end
 
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 8456195e6..63c064d84 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -144,8 +144,8 @@ In Coqlib / reference location:
 - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
   was very specific. Use tclPROGRESS instead.
 
-- The Refine.refine function and its variants now have the unsafe flag turned
-  down by default.
+- The unsafe flag of the Refine.refine function and its variants has been
+  renamed and dualized into typecheck and has been made mandatory.
 
 ** Ltac API **
 
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
index db69b08a2..8f96ac223 100644
--- a/dev/doc/proof-engine.md
+++ b/dev/doc/proof-engine.md
@@ -42,14 +42,13 @@ goal holes thanks to the `Refine` module, and in particular to the
 `Refine.refine` primitive.
 
 ```ocaml
-val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
-(** In [refine ?unsafe t], [t] is a term with holes under some
+val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
+(** In [refine typecheck t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
     raised during the interpretation of [t] are caught and result in
-    tactic failures. If [unsafe] is [false] (default is [true]) [t] is
-    type-checked beforehand. *)
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 ```
 
 In a first approximation, we can think of `'a Sigma.run` as
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 4f4e9a851..0f5b80664 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -255,7 +255,7 @@ let app_global_with_holes f args n =
     Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
-    Refine.refine ~unsafe:true begin fun sigma ->
+    Refine.refine ~typecheck:false begin fun sigma ->
       let t = Tacmach.New.pf_get_type_of gl fc in
       let t = Termops.prod_applist sigma t (Array.to_list args) in
       let ans = mkApp (fc, args) in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 18d7b818c..7259faecd 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -365,7 +365,7 @@ let refine_tac ist simple with_classes c =
     let update = begin fun sigma ->
       c env sigma
     end in
-    let refine = Refine.refine ~unsafe:true update in
+    let refine = Refine.refine ~typecheck:false update in
     if simple then refine
     else refine <*>
            Tactics.New.reduce_after_refine <*>
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3927ca7ce..fad181c89 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1539,7 +1539,7 @@ let assert_replacing id newt tac =
     | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
-    Refine.refine ~unsafe:false begin fun sigma ->
+    Refine.refine ~typecheck:true begin fun sigma ->
       let (sigma, ev) = Evarutil.new_evar env' sigma concl in
       let (sigma, ev') = Evarutil.new_evar env sigma newt in
       let map d =
@@ -1573,7 +1573,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	match clause, prf with
 	| Some id, Some p ->
             let tac = tclTHENLIST [
-              Refine.refine ~unsafe:false (fun h -> (h,p));
+              Refine.refine ~typecheck:true (fun h -> (h,p));
               Proofview.Unsafe.tclNEWGOALS gls;
             ] in
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1590,7 +1590,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
               let (sigma, ev) = Evarutil.new_evar env sigma newt in
               (sigma, mkApp (p, [| ev |]))
             end in
-            Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
+            Refine.refine ~typecheck:true make <*> Proofview.Unsafe.tclNEWGOALS gls
             end
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index fb03948ba..440a10bfb 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -652,7 +652,7 @@ let clever_rewrite_base_poly typ p result theorem =
   let full = pf_concl gl in
   let env = pf_env gl in
   let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
-  Refine.refine ~unsafe:true begin fun sigma ->
+  Refine.refine ~typecheck:false begin fun sigma ->
   let t =
     applist
       (mkLambda
@@ -688,7 +688,7 @@ let clever_rewrite_gen_nat p result (t,args) =
 (** Solve using the term the term [t _] *)
 let refine_app gl t =
   let open Tacmach.New in
-  Refine.refine ~unsafe:true begin fun sigma ->
+  Refine.refine ~typecheck:false begin fun sigma ->
   let env = pf_env gl in
   let ht = match EConstr.kind sigma (pf_get_type_of gl t) with
   | Prod (_, t, _) -> t
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 4a9dddd2b..7ae9e3824 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -95,7 +95,7 @@ let ssrmkabs id gl =
   end in
   Proofview.V82.of_tactic
     (Proofview.tclTHEN
-      (Tactics.New.refine step)
+      (Tactics.New.refine ~typecheck:false step)
       (Proofview.tclFOCUS 1 3 Proofview.shelve)) gl
 
 let ssrmkabstac ids =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index eab053f3a..796b4b837 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -69,7 +69,7 @@ let add_side_effect env = function
 let add_side_effects env effects =
   List.fold_left (fun env eff -> add_side_effect env eff) env effects
 
-let generic_refine ?(unsafe = false) f gl =
+let generic_refine ~typecheck f gl =
   let gl = Proofview.Goal.assume gl in
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
@@ -91,9 +91,9 @@ let generic_refine ?(unsafe = false) f gl =
   let env = add_side_effects env sideff in
   (** Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
-  let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
+  let sigma = if typecheck then CList.fold_left fold sigma evs else sigma in
   (** Check that the refined term is typesafe *)
-  let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
+  let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
   (** Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
@@ -132,16 +132,16 @@ let lift c =
   Proofview.tclUNIT c
   end
 
-let make_refine_enter ?unsafe f gl = generic_refine ?unsafe (lift f) gl
+let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl
 
-let refine_one ?(unsafe = false) f =
-  Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
+let refine_one ~typecheck f =
+  Proofview.Goal.enter_one (make_refine_enter ~typecheck f)
 
-let refine ?(unsafe = false) f =
+let refine ~typecheck f =
   let f evd =
     let (evd,c) = f evd in (evd,((), c))
   in
-  Proofview.Goal.enter (make_refine_enter ~unsafe f)
+  Proofview.Goal.enter (make_refine_enter ~typecheck f)
 
 (** Useful definitions *)
 
@@ -153,7 +153,7 @@ let with_type env evd c t =
   in
   evd , j'.Environ.uj_val
 
-let refine_casted ?unsafe f = Proofview.Goal.enter begin fun gl ->
+let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl ->
   let gl = Proofview.Goal.assume gl in
   let concl = Proofview.Goal.concl gl in
   let env = Proofview.Goal.env gl in
@@ -161,7 +161,7 @@ let refine_casted ?unsafe f = Proofview.Goal.enter begin fun gl ->
     let (h, c) = f h in
     with_type env h c concl
   in
-  refine ?unsafe f
+  refine ~typecheck f
 end
 
 (** {7 solve_constraints}
diff --git a/proofs/refine.mli b/proofs/refine.mli
index cede9d458..c1c57ecb8 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -21,19 +21,18 @@ val pr_constr :
 
 (** {7 Refinement primitives} *)
 
-val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
-(** In [refine ?unsafe t], [t] is a term with holes under some
+val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+(** In [refine ~typecheck t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
     raised during the interpretation of [t] are caught and result in
-    tactic failures. If [unsafe] is [false] (which is the default) [t] is
-    type-checked beforehand. *)
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 
-val refine_one : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
+val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
 (** A variant of [refine] which assumes exactly one goal under focus *)
 
-val generic_refine : ?unsafe:bool -> ('a * EConstr.t) tactic ->
+val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
   [ `NF ] Proofview.Goal.t -> 'a tactic
 (** The general version of refine. *)
 
@@ -44,7 +43,7 @@ val with_type : Environ.env -> Evd.evar_map ->
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)
 
-val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)
 
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 425b88ee7..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 ~unsafe:true (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 9f03191cf..cde891290 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -163,7 +163,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 +200,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 +222,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 +293,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 +323,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 +377,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 +527,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 ~unsafe:true 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
@@ -579,7 +579,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 ~unsafe:true 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
@@ -1225,7 +1225,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 +1666,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 +1914,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 ~unsafe:true 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 +1934,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 +1959,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 ~unsafe:true 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 +2076,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 +2128,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 ~unsafe:true 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 +2149,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 ~unsafe:true 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 +2888,7 @@ let new_generalize_gen_let lconstr =
 	0 lconstr (concl, sigma, [])
     in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-	(Refine.refine ~unsafe:true 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 +3598,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 ~unsafe:true 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 +4418,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 +4441,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
@@ -5101,7 +5101,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
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3cd0a8de8..aba61146c 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 		if not (Option.is_empty term) then
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
-                      Refine.refine ~unsafe:true (fun evm -> (evm,EConstr.of_constr (Option.get term)));
+                      Refine.refine ~typecheck:false (fun evm -> (evm,EConstr.of_constr (Option.get term)));
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]