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

(limited to 'plugins/cc/ccalgo.mli')

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