diff options
Diffstat (limited to 'contrib/cc/ccalgo.mli')
| -rw-r--r-- | contrib/cc/ccalgo.mli | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli index 05a5c4d1..cdc0065e 100644 --- a/contrib/cc/ccalgo.mli +++ b/contrib/cc/ccalgo.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccalgo.mli 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: ccalgo.mli 10579 2008-02-21 13:54:00Z corbinea $ *) open Util open Term @@ -19,10 +19,16 @@ type cinfo = type term = Symb of constr - | Eps + | Product of sorts_family * sorts_family + | Eps of identifier | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) +type patt_kind = + Normal + | Trivial of types + | Creates_variables + type ccpattern = PApp of term * ccpattern list | PVar of int @@ -70,7 +76,7 @@ val axioms : forest -> (constr, term * term) Hashtbl.t val epsilons : forest -> pa_constructor list -val empty : int -> state +val empty : int -> Proof_type.goal Tacmach.sigma -> state val add_term : state -> term -> int @@ -79,8 +85,7 @@ val add_equality : state -> constr -> term -> term -> unit val add_disequality : state -> from -> term -> term -> unit val add_quant : state -> identifier -> bool -> - int * bool * ccpattern * bool * ccpattern -> unit - + int * patt_kind * ccpattern * patt_kind * ccpattern -> unit val tail_pac : pa_constructor -> pa_constructor @@ -102,9 +107,9 @@ type quant_eq= qe_pol: bool; qe_nvars:int; qe_lhs: ccpattern; - qe_lhs_valid:bool; + qe_lhs_valid:patt_kind; qe_rhs: ccpattern; - qe_rhs_valid:bool} + qe_rhs_valid:patt_kind} type pa_fun= |