diff options
Diffstat (limited to 'tactics/nbtermdn.mli')
-rw-r--r-- | tactics/nbtermdn.mli | 55 |
1 files changed, 34 insertions, 21 deletions
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli index e8279b76f..027ea5734 100644 --- a/tactics/nbtermdn.mli +++ b/tactics/nbtermdn.mli @@ -15,24 +15,37 @@ open Libnames (*i*) (* Named, bounded-depth, term-discrimination nets. *) - -type ('na,'a) t -type ('na,'a) frozen_t - -val create : unit -> ('na,'a) t - -val add : ('na,'a) t -> ('na * (constr_pattern * 'a)) -> unit -val rmv : ('na,'a) t -> 'na -> unit -val in_dn : ('na,'a) t -> 'na -> bool -val remap : ('na,'a) t -> 'na -> (constr_pattern * 'a) -> unit - -val lookup : ('na,'a) t -> constr -> (constr_pattern * 'a) list -val app : ('na -> (constr_pattern * 'a) -> unit) -> ('na,'a) t -> unit - -val dnet_depth : int ref - -val freeze : ('na,'a) t -> ('na,'a) frozen_t -val unfreeze : ('na,'a) frozen_t -> ('na,'a) t -> unit -val empty : ('na,'a) t -> unit -val to2lists : ('na,'a) t -> ('na * (constr_pattern * 'a)) list * - (Termdn.term_label option * 'a Btermdn.t) list +module Make : + functor (Y:Map.OrderedType) -> +sig + + module Term_dn : sig + type term_label = + | GRLabel of global_reference + | ProdLabel + | LambdaLabel + | SortLabel of sorts option + end + + type 'na t + type 'na frozen_t + + val create : unit -> 'na t + + val add : 'na t -> ('na * (constr_pattern * Y.t)) -> unit + val rmv : 'na t -> 'na -> unit + val in_dn : 'na t -> 'na -> bool + val remap : 'na t -> 'na -> (constr_pattern * Y.t) -> unit + + val lookup : 'na t -> constr -> (constr_pattern * Y.t) list + val app : ('na -> (constr_pattern * Y.t) -> unit) -> 'na t -> unit + + val dnet_depth : int ref + + + val freeze : 'na t -> 'na frozen_t + val unfreeze : 'na frozen_t -> 'na t -> unit + val empty : 'na t -> unit + val to2lists : 'na t -> ('na * (constr_pattern * Y.t)) list * + (Term_dn.term_label option * Btermdn.Make(Y).t) list +end |