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

5 files changed, 8 insertions, 8 deletions

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 =