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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/cc')

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
-- 
cgit v1.2.3


From 0fad09306982a88ff8d633d36abdc440dd542ab3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 13 Jun 2017 10:33:56 +0200
Subject: Dualize the unsafe flag of refine into typecheck and make it
 mandatory.

---
 plugins/cc/cctac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 4f4e9a8518..0f5b806644 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
-- 
cgit v1.2.3


From 0437339ccac602d692b5b8c071b77ac756805520 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Jun 2017 16:41:09 +0200
Subject: Removing Proof_type from the API.

Unluckily, this forces replacing a lot of code in plugins, because the API
defined the type of goals and tactics in Proof_type, and by the no-alias rule,
this was the only one. But Proof_type was already implicitly deprecated, so
that the API should have relied on Tacmach instead.
---
 plugins/cc/ccalgo.ml  | 2 +-
 plugins/cc/ccalgo.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 5c7cad7ff5..39fb8feeb8 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -270,7 +270,7 @@ type state =
      mutable rew_depth:int;
      mutable changed:bool;
      by_type: Int.Set.t Typehash.t;
-     mutable gls:Proof_type.goal Evd.sigma}
+     mutable gls:Goal.goal Evd.sigma}
 
 let dummy_node =
   {
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 505029992a..51e2301fe6 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -129,7 +129,7 @@ val axioms : forest -> (term * term) Constrhash.t
 
 val epsilons : forest -> pa_constructor list
 
-val empty : int -> Proof_type.goal Evd.sigma -> state
+val empty : int -> Goal.goal Evd.sigma -> state
 
 val add_term : state -> term -> int
 
-- 
cgit v1.2.3