Explicit the unsafe flag of all calls to Refine.refine.

5 files changed, 13 insertions, 13 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 1ce1660b3..4f4e9a851 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 begin fun sigma ->
+    Refine.refine ~unsafe:true 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/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 9cb94b68d..fb03948ba 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 begin fun sigma ->
+  Refine.refine ~unsafe:true 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 begin fun sigma ->
+  Refine.refine ~unsafe:true 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/tactics/inv.ml b/tactics/inv.ml
index ec038f638..425b88ee7 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 ~unsafe:true (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 b553f316c..9f03191cf 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -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 begin fun sigma ->
+  Refine.refine ~unsafe:true 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 begin fun sigma ->
+  Refine.refine ~unsafe:true 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
@@ -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 begin fun sigma ->
+        Refine.refine ~unsafe:true 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
@@ -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 begin fun sigma ->
+  Refine.refine ~unsafe:true 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
@@ -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 begin fun sigma ->
+    Refine.refine ~unsafe:true 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 begin fun sigma ->
+      Refine.refine ~unsafe:true 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 begin fun sigma ->
+	(Refine.refine ~unsafe:true 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 begin fun sigma ->
+  Refine.refine ~unsafe:true begin fun sigma ->
   let eqslen = List.length eqs in
     (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
   let sigma, abshypeq, abshypt =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 8e6a0f6a7..3cd0a8de8 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 (fun evm -> (evm,EConstr.of_constr (Option.get term)));
+                      Refine.refine ~unsafe:true (fun evm -> (evm,EConstr.of_constr (Option.get term)));
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]