diff options
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 + |