1 files changed, 35 insertions, 22 deletions
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 579b24d4..027ea573 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nbtermdn.mli 6427 2004-12-07 17:41:10Z sacerdot $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Term
@@ -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 * 
-                             (global_reference 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