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 5c7cad7ff..39fb8feeb 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 505029992..51e2301fe 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