From 6332f43dfee3efc890c5f8fdc1b5b54942c16307 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 9 May 2017 09:55:40 +0200
Subject: Explicit the unsafe flag of all calls to Refine.refine.

---
 plugins/cc/cctac.ml        | 2 +-
 plugins/omega/coq_omega.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 1ce1660b32..4f4e9a8518 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 9cb94b68df..fb03948ba1 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
-- 
cgit v1.2.3