diff options
Diffstat (limited to 'plugins/cc/ccalgo.mli')
| -rw-r--r-- | plugins/cc/ccalgo.mli | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index c7fa2f56..4ebc6a13 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -1,13 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util -open Term +open Constr open Names type pa_constructor = @@ -30,7 +32,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 *) @@ -85,7 +87,7 @@ type representative= mutable lfathers:Int.Set.t; mutable fathers:Int.Set.t; mutable inductive_status: inductive_status; - class_type : Term.types; + class_type : types; mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality @@ -120,7 +122,7 @@ val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : (unit -> Pp.std_ppcmds) -> unit +val debug : (unit -> Pp.t) -> unit val forest : state -> forest @@ -128,7 +130,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 -> Goal.goal Evd.sigma -> state val add_term : state -> term -> int @@ -169,7 +171,7 @@ val find_instances : state -> (quant_eq * int array) list val execute : bool -> state -> explanation option -val pr_idx_term : forest -> int -> Pp.std_ppcmds +val pr_idx_term : forest -> int -> Pp.t val empty_forest: unit -> forest |