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

5 files changed, 24 insertions, 43 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3b99cc5b9e..9bb55977ec 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -145,7 +145,7 @@ let rebuild_dn st ((l,l',dn) : search_entry) =
 
 
 let lookup_tacs (hdc,c) st (l,l',dn) =
-  let l'  = List.map snd (Bounded_net.lookup st dn c) in
+  let l'  = Bounded_net.lookup st dn c in
   let sl' = List.stable_sort pri_order_int l' in
     List.merge pri_order_int l sl'
 
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index b93be6fc28..9492ae1a0a 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -130,17 +130,12 @@ module Make =
   functor (Z : Map.OrderedType) ->
 struct
 
-  module X = struct
-    type t = constr_pattern*int
-    let compare = Pervasives.compare (** FIXME *)
-  end
-
  module Y = struct
     type t = term_label
     let compare = compare_term_label
  end
 
- module Dn = Dn.Make(X)(Y)(Z)
+ module Dn = Dn.Make(Y)(Z)
 
  type t = Dn.t
 
@@ -165,16 +160,12 @@ struct
   let lookup = function
     | None ->
 	(fun dn t ->
-	   List.map
-	     (fun ((c,_),v) -> (c,v))
-	     (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)))
+	     Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))
     | Some st ->
 	(fun dn t ->
-	   List.map
-	     (fun ((c,_),v) -> (c,v))
-	     (Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth)))
+	     Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth))
 
-  let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn
+  let app f dn = Dn.app f dn
 
 end
 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 5755020269..d913301384 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -33,9 +33,8 @@ sig
   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
+  val lookup : transparent_state option -> t -> constr -> Z.t list
+  val app : (Z.t -> unit) -> t -> unit
 end
-    
-val dnet_depth : int ref
 
+val dnet_depth : int ref
diff --git a/tactics/dn.ml b/tactics/dn.ml
index e0f2016c77..3b1614d6ce 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -3,7 +3,6 @@ open Util
 type 'res lookup_res = Label of 'res | Nothing | Everything
 
 module Make =
-  functor (X : Set.OrderedType) ->
     functor (Y : Map.OrderedType) ->
       functor (Z : Map.OrderedType) ->
 struct
@@ -21,26 +20,19 @@ struct
 	| Some(l,n),None -> 1
 	| None, Some(l,n) -> -1
   end
-  module XZOrd = struct
-    type t = X.t * Z.t
-    let compare (x1,x2) (y1,y2) =
-      let m = (X.compare x1 y1) in
-      if Int.equal m 0 then (Z.compare x2 y2) else
-	m
-  end
-  module XZ = Set.Make(XZOrd)
+  module ZSet = Set.Make(Z)
   module X_tries =
   struct
-    type t = XZ.t
-    let nil = XZ.empty
-    let is_nil = XZ.is_empty
-    let add = XZ.union
-    let sub = XZ.diff
+    type t = ZSet.t
+    let nil = ZSet.empty
+    let is_nil = ZSet.is_empty
+    let add = ZSet.union
+    let sub = ZSet.diff
   end
 
   module Trie = Trie.Make(Y_tries)(X_tries)
 
-  type  decompose_fun = X.t -> (Y.t * X.t list) option
+  type 'a decompose_fun = 'a -> (Y.t * 'a list) option
 
   type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res
 
@@ -95,15 +87,15 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
 		 (tm_of tm (Some(lbl,List.length v))) v)
 	| Everything -> skip_arg 1 tm
     in
-    List.flatten (List.map (fun (tm,b) -> XZ.elements (Trie.get tm)) (lookrec t tm))
+    List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm))
 
   let add tm dna (pat,inf) =
-    let p = path_of dna pat in Trie.add p (XZ.singleton (pat, inf)) tm
+    let p = path_of dna pat in Trie.add p (ZSet.singleton inf) tm
 
   let rmv tm dna (pat,inf) =
-    let p = path_of dna pat in Trie.remove p (XZ.singleton (pat, inf)) tm
+    let p = path_of dna pat in Trie.remove p (ZSet.singleton inf) tm
 
-  let app f tm = Trie.iter (fun _ p -> XZ.iter f p) tm
+  let app f tm = Trie.iter (fun _ p -> ZSet.iter f p) tm
 
 end
 
diff --git a/tactics/dn.mli b/tactics/dn.mli
index bab925a20c..78896ae9ab 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