diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /tactics/btermdn.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'tactics/btermdn.mli')
-rw-r--r-- | tactics/btermdn.mli | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 959f7d10..ebded23a 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: btermdn.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Term @@ -15,15 +15,19 @@ open Names (*i*) (* Discrimination nets with bounded depth. *) +module Make : + functor (Z : Map.OrderedType) -> +sig + type t -type 'a t + val create : unit -> t -val create : unit -> 'a t - -val add : transparent_state option -> 'a t -> (constr_pattern * 'a) -> 'a t -val rmv : transparent_state option -> 'a t -> (constr_pattern * 'a) -> 'a t - -val lookup : transparent_state option -> 'a t -> constr -> (constr_pattern * 'a) list -val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit + val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t + val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t + val lookup : transparent_state option -> t -> constr -> (constr_pattern * Z.t) list + val app : ((constr_pattern * Z.t) -> unit) -> t -> unit +end + val dnet_depth : int ref + |