diff options
Diffstat (limited to 'plugins/cc/ccalgo.mli')
-rw-r--r-- | plugins/cc/ccalgo.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index c7fa2f56f..505029992 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Util open Term open Names @@ -30,7 +31,7 @@ type cinfo = type term = Symb of constr - | Product of sorts * sorts + | Product of Sorts.t * Sorts.t | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) @@ -128,7 +129,7 @@ val axioms : forest -> (term * term) Constrhash.t val epsilons : forest -> pa_constructor list -val empty : int -> Proof_type.goal Tacmach.sigma -> state +val empty : int -> Proof_type.goal Evd.sigma -> state val add_term : state -> term -> int |