diff options
author | 2013-05-08 18:03:54 +0200 | |
---|---|---|
committer | 2013-05-08 18:03:54 +0200 | |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /plugins/cc/ccalgo.mli | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'plugins/cc/ccalgo.mli')
-rw-r--r-- | plugins/cc/ccalgo.mli | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 8786c907..9653da2c 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccalgo.mli 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Term open Names @@ -24,6 +22,8 @@ type term = | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) +val term_equal : term -> term -> bool + type patt_kind = Normal | Trivial of types @@ -66,13 +66,16 @@ type explanation = | Contradiction of disequality | Incomplete +module Constrhash : Hashtbl.S with type key = constr +module Termhash : Hashtbl.S with type key = term + val constr_of_term : term -> constr val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit val forest : state -> forest -val axioms : forest -> (constr, term * term) Hashtbl.t +val axioms : forest -> (term * term) Constrhash.t val epsilons : forest -> pa_constructor list @@ -127,7 +130,7 @@ val do_match : state -> val init_pb_stack : state -> matching_problem Stack.t -val paf_of_patt : (term, int) Hashtbl.t -> ccpattern -> pa_fun +val paf_of_patt : int Termhash.t -> ccpattern -> pa_fun val find_instances : state -> (quant_eq * int array) list |