Term dnets do no need to contain the afferent constr pattern in their nodes.

1 files changed, 5 insertions, 6 deletions

diff --git a/tactics/dn.mli b/tactics/dn.mli
index bab925a20..78896ae9a 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -2,12 +2,11 @@ type 'res lookup_res = Label of 'res | Nothing | Everything
 
 
 module Make :
-  functor (X : Set.OrderedType) ->
     functor (Y : Map.OrderedType) ->
       functor (Z : Map.OrderedType) ->
 sig
 
-  type decompose_fun = X.t -> (Y.t * X.t list) option
+  type 'a decompose_fun = 'a -> (Y.t * 'a list) option
 
   type t
 
@@ -19,9 +18,9 @@ sig
      must decompose any tree into a label characterizing its root node and
      the list of its subtree *)
 
-  val add : t -> decompose_fun -> X.t * Z.t -> t
+  val add : t -> 'a decompose_fun -> 'a * Z.t -> t
 
-  val rmv : t -> decompose_fun -> X.t * Z.t -> t
+  val rmv : t -> 'a decompose_fun -> 'a * Z.t -> t
 
   type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res
 
@@ -33,9 +32,9 @@ sig
    characterizing its root node and the list of its subtree *)
 
   val lookup : t -> 'term lookup_fun -> 'term
-    -> (X.t * Z.t) list
+    -> Z.t list
 
-  val app : ((X.t * Z.t) -> unit) -> t -> unit
+  val app : (Z.t -> unit) -> t -> unit
 
   val skip_arg : int -> t -> (t * bool) list