Imported Upstream version 8.5~beta1+dfsg

1 files changed, 16 insertions, 25 deletions

diff --git a/tactics/dn.mli b/tactics/dn.mli
index 662ac19a..20407e9d 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -1,48 +1,39 @@
+type 'res lookup_res = Label of 'res | Nothing | Everything
 
 
-
-
-
-
-
-module Make : 
-  functor (X : Set.OrderedType) ->
+module Make :
     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
 
   val create : unit -> t
-    
+
   (** [add t f (tree,inf)] adds a structured object [tree] together with
      the associated information [inf] to the table [t]; the function
      [f] is used to translated [tree] into its prefix decomposition: [f]
      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 rmv : t -> decompose_fun -> X.t * Z.t -> t
-    
-  type 'res lookup_res = Label of 'res | Nothing | Everything
-      
+
+  val add : t -> 'a decompose_fun -> 'a * Z.t -> t
+
+  val rmv : t -> 'a decompose_fun -> 'a * Z.t -> t
+
   type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res
-    
+
 
 (** [lookup t f tree] looks for trees (and their associated
    information) in table [t] such that the structured object [tree]
    matches against them; [f] is used to translated [tree] into its
    prefix decomposition: [f] must decompose any tree into a label
    characterizing its root node and the list of its subtree *)
-    
+
   val lookup : t -> 'term lookup_fun -> 'term
-    -> (X.t * Z.t) list
-    
-  val app : ((X.t * Z.t) -> unit) -> t -> unit
-    
-  val skip_arg : int -> t -> (t * bool) list
-    
+    -> Z.t list
+
+  val app : (Z.t -> unit) -> t -> unit
+
 end