15 files changed, 514 insertions, 311 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9cdbc66278..fafc0b5920 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -89,28 +89,30 @@ let insert v l =
 
 type stored_data = pri_auto_tactic
 
-type search_entry = stored_data list * stored_data list * stored_data Btermdn.t
+module Bounded_net = Btermdn.Make(struct
+				    type t = stored_data
+				    let compare = Pervasives.compare
+				  end)
 
-let empty_se = ([],[],Btermdn.create ())
+type search_entry = stored_data list * stored_data list * Bounded_net.t
+
+let empty_se = ([],[],Bounded_net.create ())
 
 let add_tac pat t st (l,l',dn) =
   match pat with
   | None -> if not (List.mem t l) then (insert t l, l', dn) else (l, l', dn)
-  | Some pat -> if not (List.mem t l') then (l, insert t l', Btermdn.add st dn (pat,t)) else (l, l', dn)
+  | Some pat -> if not (List.mem t l') then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn)
 
 let rebuild_dn st (l,l',dn) =
-  (l, l', List.fold_left (fun dn t -> Btermdn.add (Some st) dn (Option.get t.pat, t))
-    (Btermdn.create ()) l')
+  (l, l', List.fold_left (fun dn t -> Bounded_net.add (Some st) dn (Option.get t.pat, t))
+    (Bounded_net.create ()) l')
 
 let lookup_tacs (hdc,c) st (l,l',dn) =
-  let l'  = List.map snd (Btermdn.lookup st dn c) in
+  let l'  = List.map snd (Bounded_net.lookup st dn c) in
   let sl' = Sort.list pri_order l' in
     Sort.merge pri_order l sl'
 
-module Constr_map = Map.Make(struct
-			       type t = global_reference
-			       let compare = Pervasives.compare
-			     end)
+module Constr_map = Map.Make(RefOrdered)
 
 let is_transparent_gr (ids, csts) = function
   | VarRef id -> Idpred.mem id ids
@@ -389,14 +391,8 @@ let forward_subst_tactic =
 
 let set_extern_subst_tactic f = forward_subst_tactic := f
 
-let subst_autohint (_,subst,(local,name,hintlist as obj)) =
+let subst_autohint (subst,(local,name,hintlist as obj)) = 
   let trans_clenv clenv = Clenv.subst_clenv subst clenv in
-  let trans_data data code =
-    { data with
-	pat = Option.smartmap (subst_pattern subst) data.pat ;
-	code = code ;
-    }
-  in
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
     let gr' =
@@ -409,29 +405,49 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
     let data' = match data.code with
       | Res_pf (c, clenv) ->
 	  let c' = subst_mps subst c in
-	    if c==c' then data else
-	      trans_data data (Res_pf (c', trans_clenv clenv))
+	  let clenv' = trans_clenv clenv in
+	  let pat' = Option.smartmap (subst_pattern subst) data.pat in
+	    if c==c' && clenv'==clenv && pat'==data.pat then data else
+	      {data with
+		 pat=pat';
+		 code=Res_pf (c', clenv')}
       | ERes_pf (c, clenv) ->
 	  let c' = subst_mps subst c in
-	    if c==c' then data else
-	      trans_data data (ERes_pf (c', trans_clenv clenv))
+	  let clenv' = trans_clenv clenv in
+	  let pat' = Option.smartmap (subst_pattern subst) data.pat in
+	    if c==c' && clenv'==clenv && pat'==data.pat then data else
+	      {data with
+		 pat=pat';
+		 code=ERes_pf (c', clenv')}
       | Give_exact c ->
 	  let c' = subst_mps subst c in
-	    if c==c' then data else
-	      trans_data data (Give_exact c')
+	  let pat' = Option.smartmap (subst_pattern subst) data.pat in
+	    if c==c' && pat'==data.pat then data else
+	      {data with
+		 pat=pat';
+		 code=(Give_exact c')}
       | Res_pf_THEN_trivial_fail (c, clenv) ->
 	  let c' = subst_mps subst c in
-	    if c==c' then data else
-	      let code' = Res_pf_THEN_trivial_fail (c', trans_clenv clenv) in
-		trans_data data code'
+	  let clenv' = trans_clenv clenv in
+	  let pat' = Option.smartmap (subst_pattern subst) data.pat in
+	    if c==c' && clenv'==clenv && pat'==data.pat then data else
+	      {data with
+		 pat=pat';
+		 code=Res_pf_THEN_trivial_fail (c',clenv')}
       | Unfold_nth ref ->
           let ref' = subst_evaluable_reference subst ref in
-           if ref==ref' then data else
-	    trans_data data (Unfold_nth ref')
+	  let pat' = Option.smartmap (subst_pattern subst) data.pat in
+           if ref==ref' && pat'==data.pat then data else
+	     {data with
+		pat=pat';
+		code=(Unfold_nth ref')}
       | Extern tac ->
 	  let tac' = !forward_subst_tactic subst tac in
-	    if tac==tac' then data else
-	      trans_data data (Extern tac')
+	  let pat' = Option.smartmap (subst_pattern subst) data.pat in
+	    if tac==tac' && pat'==data.pat then data else
+	      {data with
+		 pat=pat';
+		 code=(Extern tac')}
     in
       if k' == k && data' == data then hint else
 	(k',data')
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 1910bd139d..83ad60bc30 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -42,7 +42,7 @@ type pri_auto_tactic = {
 
 type stored_data = pri_auto_tactic
 
-type search_entry = stored_data list * stored_data list * stored_data Btermdn.t
+type search_entry
 
 (* The head may not be bound. *)
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 6abe8938c6..db0bbd867a 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -215,7 +215,8 @@ let cache_hintrewrite (_,(rbase,lrl)) =
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
     rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab
 
-let subst_hintrewrite (_,subst,(rbase,list as node)) =
+
+let subst_hintrewrite (subst,(rbase,list as node)) =
   let list' = HintDN.subst subst list in
     if list' == list then node else
       (rbase,list')
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index e28a9e3c35..198ee78595 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -20,71 +20,133 @@ open Libnames
 
 let dnet_depth = ref 8
 
-let bounded_constr_pat_discr_st st (t,depth) =
-  if depth = 0 then
-    None
-  else
-    match constr_pat_discr_st st t with
-      | None -> None
-      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 
-let bounded_constr_val_discr_st st (t,depth) =
-  if depth = 0 then
-    Dn.Nothing
-  else
-    match constr_val_discr_st st t with
-      | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
-      | Dn.Nothing -> Dn.Nothing
-      | Dn.Everything -> Dn.Everything
+module Make =
+  functor (Z : Map.OrderedType) ->
+struct
+  module Term_dn = Termdn.Make(Z)
 
-let bounded_constr_pat_discr (t,depth) =
-  if depth = 0 then
-    None
-  else
-    match constr_pat_discr t with
-      | None -> None
-      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+  module X = struct
+    type t = constr_pattern*int
+    let compare = Pervasives.compare 
+  end
 
-let bounded_constr_val_discr (t,depth) =
-  if depth = 0 then
-    Dn.Nothing
-  else
-    match constr_val_discr t with
-      | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
-      | Dn.Nothing -> Dn.Nothing
-      | Dn.Everything -> Dn.Everything
+ module Y = struct 
+     type t = Term_dn.term_label
+     let compare x y = 
+       let make_name n =
+	 match n with
+	 | Term_dn.GRLabel(ConstRef con) -> 
+	     Term_dn.GRLabel(ConstRef(constant_of_kn(canonical_con con)))
+	 | Term_dn.GRLabel(IndRef (kn,i)) ->
+	     Term_dn.GRLabel(IndRef(mind_of_kn(canonical_mind kn),i))
+	 | Term_dn.GRLabel(ConstructRef ((kn,i),j ))->
+	     Term_dn.GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j))
+	 | k -> k
+       in
+	 Pervasives.compare (make_name x) (make_name y)
+ end
+ 
+ module Dn = Dn.Make(X)(Y)(Z)
+  
+ type t = Dn.t
 
-type 'a t = (term_label,constr_pattern * int,'a) Dn.t
+  let create = Dn.create
 
-let create = Dn.create
+  let decomp = 
+    let rec decrec acc c = match kind_of_term c with
+      | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
+      | Cast (c1,_,_) -> decrec acc c1
+      | _ -> (c,acc)
+    in 
+      decrec []
 
-let add = function
-  | None ->
-      (fun dn (c,v) ->
-	Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
-  | Some st ->
-      (fun dn (c,v) ->
-	Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+  let constr_val_discr t =
+  let c, l = decomp t in
+    match kind_of_term c with
+    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
+    | Var id -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
+    | Const _ -> Dn.Everything
+    | _ -> Dn.Nothing
 
-let rmv = function
-  | None ->
-      (fun dn (c,v) ->
-	Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
-  | Some st ->
-      (fun dn (c,v) ->
-	Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+let constr_val_discr_st (idpred,cpred) t =
+  let c, l = decomp t in
+    match kind_of_term c with
+    | Const c -> if Cpred.mem c cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l)
+    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
+    | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
+    | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
+    | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
+    | Sort s -> Dn.Label(Term_dn.SortLabel (Some s), [])
+    | Evar _ -> Dn.Everything
+    | _ -> Dn.Nothing
 
-let lookup = function
-  | None ->
-      (fun dn t ->
-	List.map
-	  (fun ((c,_),v) -> (c,v))
-	  (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)))
-
-let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn
+  let bounded_constr_pat_discr_st st (t,depth) =
+    if depth = 0 then 
+      None 
+    else
+      match Term_dn.constr_pat_discr_st st t with
+	| None -> None
+	| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+	    
+  let bounded_constr_val_discr_st st (t,depth) =
+    if depth = 0 then 
+      Dn.Nothing 
+    else
+      match constr_val_discr_st st t with
+	| Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
+	| Dn.Nothing -> Dn.Nothing
+	| Dn.Everything -> Dn.Everything
 
+  let bounded_constr_pat_discr (t,depth) =
+    if depth = 0 then 
+      None 
+    else
+      match Term_dn.constr_pat_discr t with
+	| None -> None
+	| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+	    
+  let bounded_constr_val_discr (t,depth) =
+    if depth = 0 then 
+      Dn.Nothing 
+    else
+      match constr_val_discr t with
+	| Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
+	| Dn.Nothing -> Dn.Nothing
+	| Dn.Everything -> Dn.Everything
+	    
+	    
+  let add = function
+    | None -> 
+	(fun dn (c,v) -> 
+	   Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+    | Some st -> 
+	(fun dn (c,v) -> 
+	   Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+	  
+  let rmv = function
+    | None -> 
+	(fun dn (c,v) -> 
+	   Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+    | Some st -> 
+	(fun dn (c,v) -> 
+	 Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+	  
+  let lookup = function
+    | None -> 
+	(fun dn t ->
+	   List.map 
+	     (fun ((c,_),v) -> (c,v)) 
+	     (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)))
+	  
+  let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn
+    
+end
+    
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index b41ecbf77c..ebded23ac6 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -15,15 +15,19 @@ open Names
 (*i*)
 
 (* Discrimination nets with bounded depth. *)
+module Make :
+  functor (Z : Map.OrderedType) ->
+sig
+  type t
 
-type 'a t
+  val create : unit ->  t
 
-val create : unit -> 'a t
-
-val add : transparent_state option -> 'a t -> (constr_pattern * 'a) -> 'a t
-val rmv : transparent_state option -> 'a t -> (constr_pattern * 'a) -> 'a t
-
-val lookup : transparent_state option -> 'a t -> constr -> (constr_pattern * 'a) list
-val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
+  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
+end
+    
 val dnet_depth : int ref
+
diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli
index 08d97646e6..bd0859382b 100644
--- a/tactics/decl_interp.mli
+++ b/tactics/decl_interp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Tacinterp
 open Decl_expr
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 07086e05aa..96d83b9724 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -157,35 +157,44 @@ let subst_located_destructor_pattern subst = function
   | ConclLocation d ->
       ConclLocation (subst_destructor_pattern subst d)
 
+
 type destructor_data = {
   d_pat : located_destructor_pattern;
   d_pri : int;
   d_code : identifier option * glob_tactic_expr (* should be of phylum tactic *)
 }
 
-type t = (identifier,destructor_data) Nbtermdn.t
-type frozen_t = (identifier,destructor_data) Nbtermdn.frozen_t
+module Dest_data = struct 
+  type t = destructor_data
+  let compare = Pervasives.compare
+    end
+
+module Nbterm_net = Nbtermdn.Make(Dest_data)
+
+type t = identifier Nbterm_net.t
+type frozen_t = identifier Nbterm_net.frozen_t
+
+let tactab = (Nbterm_net.create () : t)
 
-let tactab = (Nbtermdn.create () : t)
+let lookup pat = Nbterm_net.lookup tactab pat
 
-let lookup pat = Nbtermdn.lookup tactab pat
 
-let init () = Nbtermdn.empty tactab
+let init () = Nbterm_net.empty tactab
 
-let freeze () = Nbtermdn.freeze tactab
-let unfreeze fs = Nbtermdn.unfreeze fs tactab
+let freeze () = Nbterm_net.freeze tactab
+let unfreeze fs = Nbterm_net.unfreeze fs tactab
 
 let add (na,dd) =
   let pat = match dd.d_pat with
     | HypLocation(_,p,_) -> p.d_typ
     | ConclLocation p -> p.d_typ
   in
-  if Nbtermdn.in_dn tactab na then begin
+  if Nbterm_net.in_dn tactab na then begin
     msgnl (str "Warning [Overriding Destructor Entry " ++
              str (string_of_id na) ++ str"]");
-    Nbtermdn.remap tactab na (pat,dd)
+    Nbterm_net.remap tactab na (pat,dd)
   end else
-    Nbtermdn.add tactab (na,(pat,dd))
+    Nbterm_net.add tactab (na,(pat,dd))
 
 let _ =
   Summary.declare_summary "destruct-hyp-concl"
@@ -207,7 +216,7 @@ let cache_dd (_,(_,na,dd)) =
 let classify_dd (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let subst_dd (_,subst,(local,na,dd)) =
+let subst_dd (subst,(local,na,dd)) =
   (local,na,
   { d_pat = subst_located_destructor_pattern subst dd.d_pat;
     d_pri = dd.d_pri;
diff --git a/tactics/dn.ml b/tactics/dn.ml
index 359e3fe7fb..8076e252c5 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -1,100 +1,99 @@
-(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *)
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
 
-(* $Id$ *)
 
-(* This file implements the basic structure of what Chet called
-   ``discrimination nets''. If my understanding is right, it serves
-   to associate actions (for example, tactics) with a priority to term
-   patterns, so that if a hypothesis matches a pattern in the net,
-   then the associated tactic is applied. Discrimination nets are used
-   (only) to implement the tactics Auto, DHyp and Point.
 
-   A discrimination net is a tries structure, that is, a tree structure
-   specially conceived for searching patterns, like for example strings
-   --see the file Tlm.ml in the directory lib/util--. Here the tries
-   structure are used for looking for term patterns.
 
-   This module is then used in :
-     - termdn.ml   (discrimination nets of terms);
-     - btermdn.ml  (discrimination nets of terms with bounded depth,
-                    used in the tactic auto);
-     - nbtermdn.ml (named discrimination nets with bounded depth, used
-                    in the tactics Dhyp and Point).
-  Eduardo (4/8/97) *)
 
-(* Definition of the basic structure *)
-
-type ('lbl,'pat) decompose_fun = 'pat -> ('lbl * 'pat list) option
-
-type 'res lookup_res = Label of 'res | Nothing | Everything
-
-type ('lbl,'tree) lookup_fun = 'tree -> ('lbl * 'tree list) lookup_res
-
-type ('lbl,'pat,'inf) t = (('lbl * int) option,'pat * 'inf) Tlm.t
-
-let create () = Tlm.empty
-
-(* [path_of dna pat] returns the list of nodes of the pattern [pat] read in
+module Make = 
+  functor (X : Set.OrderedType) ->
+    functor (Y : Map.OrderedType) ->
+      functor (Z : Map.OrderedType) ->
+struct
+  
+  module Y_tries = struct
+    type t = (Y.t * int) option
+    let compare x y = 
+      match x,y with
+	  None,None -> 0
+	| Some (l,n),Some (l',n') -> 
+	    if (Y.compare l l') = 0 && n = n' then 0 
+	    else Pervasives.compare x y
+	| a,b -> Pervasives.compare a b 
+  end
+  module X_tries = struct
+    type t = X.t * Z.t
+    let compare (x1,x2) (y1,y2) = 
+	    if (X.compare x1 y1) = 0 && (Z.compare x2 y2)=0 then 0 
+	    else Pervasives.compare (x1,x2) (y1,y2)
+  end
+
+  module T = Tries.Make(X_tries)(Y_tries)
+    
+  type  decompose_fun = X.t -> (Y.t * X.t list) option
+    
+  type 'res lookup_res = Label of 'res | Nothing | Everything
+    
+  type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res
+
+  type  t = T.t
+
+  let create () = T.empty
+
+(* [path_of dna pat] returns the list of nodes of the pattern [pat] read in 
 prefix ordering, [dna] is the function returning the main node of a pattern *)
 
-let path_of dna =
-  let rec path_of_deferred = function
-    | [] -> []
-    | h::tl -> pathrec tl h
-
-  and pathrec deferred t =
-    match dna t with
-    | None ->
-	None :: (path_of_deferred deferred)
-    | Some (lbl,[]) ->
-	(Some (lbl,0))::(path_of_deferred deferred)
-    | Some (lbl,(h::def_subl as v)) ->
-	(Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
-  in
-  pathrec []
-
-let tm_of tm lbl =
-  try [Tlm.map tm lbl, true] with Not_found -> []
-
-let rec skip_arg n tm =
-  if n = 0 then [tm,true]
-  else
-    List.flatten
-      (List.map
-	  (fun a -> match a with
-	  | None -> skip_arg (pred n) (Tlm.map tm a)
-	  | Some (lbl,m) ->
-	      skip_arg (pred n + m) (Tlm.map tm a))
-	  (Tlm.dom tm))
-
-let lookup tm dna t =
-  let rec lookrec t tm =
-    match dna t with
-    | Nothing -> tm_of tm None
-    | Label(lbl,v) ->
-	tm_of tm None@
-	  (List.fold_left
-	      (fun l c ->
+  let path_of dna =
+    let rec path_of_deferred = function
+      | [] -> []
+      | h::tl -> pathrec tl h
+	  
+    and pathrec deferred t =
+      match dna t with
+	| None -> 
+	    None :: (path_of_deferred deferred)
+	| Some (lbl,[]) ->
+	    (Some (lbl,0))::(path_of_deferred deferred)
+	| Some (lbl,(h::def_subl as v)) ->
+	    (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
+    in 
+      pathrec []
+	
+  let tm_of tm lbl =
+    try [T.map tm lbl, true] with Not_found -> []
+      
+  let rec skip_arg n tm =
+    if n = 0 then [tm,true]
+    else
+      List.flatten 
+	(List.map 
+	   (fun a -> match a with
+	      | None -> skip_arg (pred n) (T.map tm a)
+	      | Some (lbl,m) -> 
+		  skip_arg (pred n + m) (T.map tm a)) 
+	   (T.dom tm))
+	
+  let lookup tm dna t =
+    let rec lookrec t tm =
+      match dna t with
+	| Nothing -> tm_of tm None
+	| Label(lbl,v) ->
+	    tm_of tm None@
+	      (List.fold_left 
+		 (fun l c -> 
 		List.flatten(List.map (fun (tm, b) ->
-		  if b then lookrec c tm
-		  else [tm,b]) l))
-              (tm_of tm (Some(lbl,List.length v))) v)
-    | Everything -> skip_arg 1 tm
-  in
-    List.flatten (List.map (fun (tm,b) -> Tlm.xtract tm) (lookrec t tm))
-
-let add tm dna (pat,inf) =
-  let p = path_of dna pat in Tlm.add tm (p,(pat,inf))
-
-let rmv tm dna (pat,inf) =
-  let p = path_of dna pat in Tlm.rmv tm (p,(pat,inf))
-
-let app f tm = Tlm.app (fun (_,p) -> f p) tm
-
+					 if b then lookrec c tm
+					 else [tm,b]) l))
+		 (tm_of tm (Some(lbl,List.length v))) v)
+	| Everything -> skip_arg 1 tm
+    in 
+      List.flatten (List.map (fun (tm,b) -> T.xtract tm) (lookrec t tm))
+	
+  let add tm dna (pat,inf) =
+    let p = path_of dna pat in T.add tm (p,(pat,inf))
+				 
+  let rmv tm dna (pat,inf) =
+  let p = path_of dna pat in T.rmv tm (p,(pat,inf))
+			       
+  let app f tm = T.app (fun (_,p) -> f p) tm
+    
+end
+  
diff --git a/tactics/dn.mli b/tactics/dn.mli
index b4b2e6c891..3cb52a565f 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -1,46 +1,47 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
 
-(*i $Id$ i*)
 
-(* Discrimination nets. *)
 
-type ('lbl,'tree) decompose_fun = 'tree -> ('lbl * 'tree list) option
 
-type ('lbl,'pat,'inf) t (* = (('lbl * int) option,'pat * 'inf) Tlm.t *)
 
-val create : unit -> ('lbl,'pat,'inf) 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 : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf
-  -> ('lbl,'pat,'inf) t
+module Make : 
+  functor (X : Set.OrderedType) ->
+    functor (Y : Map.OrderedType) ->
+      functor (Z : Map.OrderedType) ->
+sig
 
-val rmv : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf
-  -> ('lbl,'pat,'inf) t
-
-type 'res lookup_res = Label of 'res | Nothing | Everything
-
-type ('lbl,'tree) lookup_fun = 'tree -> ('lbl * 'tree list) lookup_res
+  type decompose_fun = X.t -> (Y.t * X.t 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
+      
+  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 : ('lbl,'pat,'inf) t -> ('lbl,'term) lookup_fun -> 'term
-  -> ('pat * 'inf) list
-
-val app : (('pat * 'inf) -> unit) -> ('lbl,'pat,'inf) t -> unit
-
-val skip_arg : int -> ('lbl,'pat,'inf) t -> (('lbl,'pat,'inf) t * bool) list
+    
+  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
+    
+end
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 6ac35317cb..58ab6dfa0c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -401,7 +401,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
   else
     transitivity_right_table := lem :: !transitivity_right_table
 
-let subst_transitivity_lemma (_,subst,(b,ref)) = (b,subst_mps subst ref)
+let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
 
 let (inTransitivity,_) =
   declare_object {(default_object "TRANSITIVITY-STEPS") with
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 3fd5236a81..7d6e1c4c90 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -26,34 +26,64 @@ open Libnames
 (* The former comments are from Chet.
    See the module dn.ml for further explanations.
    Eduardo (5/8/97) *)
-
-type ('na,'a) t = {
-  mutable table : ('na,constr_pattern * 'a) Gmap.t;
-  mutable patterns : (Termdn.term_label option,'a Btermdn.t) Gmap.t }
-
-type ('na,'a) frozen_t =
-    ('na,constr_pattern * 'a) Gmap.t
-    * (Termdn.term_label option,'a Btermdn.t) Gmap.t
+module Make = 
+  functor (Y:Map.OrderedType) ->
+struct
+  module X = struct
+    type t = constr_pattern*int
+    let compare = Pervasives.compare
+  end
+
+  module Term_dn = Termdn.Make(Y)
+  open Term_dn
+  module Z = struct 
+     type t = Term_dn.term_label
+     let compare x y =  
+       let make_name n =
+	 match n with
+	 | GRLabel(ConstRef con) -> 
+	     GRLabel(ConstRef(constant_of_kn(canonical_con con)))
+	 | GRLabel(IndRef (kn,i)) ->
+	     GRLabel(IndRef(mind_of_kn(canonical_mind kn),i))
+	 | GRLabel(ConstructRef ((kn,i),j ))->
+	     GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j))
+	 | k -> k
+       in
+	 Pervasives.compare (make_name x) (make_name y)
+  end
+
+  module Dn = Dn.Make(X)(Z)(Y)
+  module Bounded_net = Btermdn.Make(Y)
+
+    
+type 'na t = {
+  mutable table : ('na,constr_pattern * Y.t) Gmap.t;
+  mutable patterns : (Term_dn.term_label option,Bounded_net.t) Gmap.t }
+
+
+type 'na frozen_t = 
+    ('na,constr_pattern * Y.t) Gmap.t
+    * (Term_dn.term_label option, Bounded_net.t) Gmap.t
 
 let create () =
   { table = Gmap.empty;
     patterns = Gmap.empty }
 
 let get_dn dnm hkey =
-  try Gmap.find hkey dnm with Not_found -> Btermdn.create ()
+  try Gmap.find hkey dnm with Not_found -> Bounded_net.create ()
 
 let add dn (na,(pat,valu)) =
-  let hkey = Option.map fst (Termdn.constr_pat_discr pat) in
+  let hkey = Option.map fst (Term_dn.constr_pat_discr pat) in 
   dn.table <- Gmap.add na (pat,valu) dn.table;
   let dnm = dn.patterns in
-  dn.patterns <- Gmap.add hkey (Btermdn.add None (get_dn dnm hkey) (pat,valu)) dnm
+  dn.patterns <- Gmap.add hkey (Bounded_net.add None (get_dn dnm hkey) (pat,valu)) dnm
 
 let rmv dn na =
   let (pat,valu) = Gmap.find na dn.table in
-  let hkey = Option.map fst (Termdn.constr_pat_discr pat) in
+  let hkey = Option.map fst (Term_dn.constr_pat_discr pat) in 
   dn.table <- Gmap.remove na dn.table;
   let dnm = dn.patterns in
-  dn.patterns <- Gmap.add hkey (Btermdn.rmv None (get_dn dnm hkey) (pat,valu)) dnm
+  dn.patterns <- Gmap.add hkey (Bounded_net.rmv None (get_dn dnm hkey) (pat,valu)) dnm
 
 let in_dn dn na = Gmap.mem na dn.table
 
@@ -61,13 +91,43 @@ let remap ndn na (pat,valu) =
   rmv ndn na;
   add ndn (na,(pat,valu))
 
+let decomp = 
+  let rec decrec acc c = match kind_of_term c with
+    | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
+    | Cast (c1,_,_) -> decrec acc c1
+    | _ -> (c,acc)
+  in 
+  decrec []
+
+  let constr_val_discr t =
+  let c, l = decomp t in
+    match kind_of_term c with
+    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
+    | Var id -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
+    | Const _ -> Dn.Everything
+    | _ -> Dn.Nothing
+
+let constr_val_discr_st (idpred,cpred) t =
+  let c, l = decomp t in
+    match kind_of_term c with
+    | Const c -> if Cpred.mem c cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l)
+    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
+    | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
+    | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
+    | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
+    | Sort s -> Dn.Label(Term_dn.SortLabel (Some s), [])
+    | Evar _ -> Dn.Everything
+    | _ -> Dn.Nothing
+
 let lookup dn valu =
   let hkey =
-    match (Termdn.constr_val_discr valu) with
+    match (constr_val_discr valu) with
     | Dn.Label(l,_) -> Some l
     | _ -> None
   in
-  try Btermdn.lookup None (Gmap.find hkey dn.patterns) valu with Not_found -> []
+  try Bounded_net.lookup None (Gmap.find hkey dn.patterns) valu with Not_found -> []
 
 let app f dn = Gmap.iter f dn.table
 
@@ -85,4 +145,4 @@ let empty dn =
 
 let to2lists dn =
   (Gmap.to_list dn.table, Gmap.to_list dn.patterns)
-
+end
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index e8279b76f4..027ea57345 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
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a7d0413230..10d2a026e7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2837,9 +2837,9 @@ let cache_md x = load_md 1 x
 let subst_kind subst id =
   match id with
     | NewTac _ -> id
-    | UpdateTac kn -> UpdateTac (Mod_subst.subst_kn subst kn)
+    | UpdateTac kn -> UpdateTac (subst_kn subst kn)
 
-let subst_md (_,subst,defs) =
+let subst_md (subst,defs) =
   List.map (fun (id,t) -> (subst_kind subst id,subst_tactic subst t)) defs
 
 let (inMD,outMD) =
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 5084635e80..a2bc950442 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -20,14 +20,43 @@ open Nametab
 (* Discrimination nets of terms.
    See the module dn.ml for further explanations.
    Eduardo (5/8/97) *)
+module Make =
+  functor (Z : Map.OrderedType) ->
+struct
 
-type term_label =
+  module X = struct
+    type t = constr_pattern
+    let compare = Pervasives.compare
+  end
+
+type term_label = 
   | GRLabel of global_reference
   | ProdLabel
   | LambdaLabel
   | SortLabel of sorts option
 
-type 'a t = (term_label,constr_pattern,'a) Dn.t
+  module Y =  struct 
+     type t = term_label
+        let compare x y = 
+       let make_name n =
+	 match n with
+	 | GRLabel(ConstRef con) -> 
+	     GRLabel(ConstRef(constant_of_kn(canonical_con con)))
+	 | GRLabel(IndRef (kn,i)) ->
+	     GRLabel(IndRef(mind_of_kn(canonical_mind kn),i))
+	 | GRLabel(ConstructRef ((kn,i),j ))->
+	     GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j))
+	 | k -> k
+       in
+	 Pervasives.compare (make_name x) (make_name y)
+  end
+       
+      
+  module Dn = Dn.Make(X)(Y)(Z)
+      
+  type t = Dn.t
+
+  type 'a lookup_res = 'a Dn.lookup_res
 
 (*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*)
 
@@ -109,3 +138,5 @@ let rmv dn st = Dn.rmv dn (constr_pat_discr_st st)
 let lookup dn st t = Dn.lookup dn (constr_val_discr_st st) t
 
 let app f dn = Dn.app f dn
+
+end
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index e60aea6b43..aea49b0735 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -28,38 +28,45 @@ indicates which constants and variables can be considered as rigid.
 These dnets are able to cope with existential variables as well, which match
 [Everything]. *)
 
-type 'a t
-
-val create : unit -> 'a t
-
-(* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *)
-
-val add : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t
-
-val rmv : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t
-
-(* [lookup t c] looks for patterns (with their action) matching term [c] *)
-
-val lookup : 'a t -> transparent_state -> constr -> (constr_pattern * 'a) list
-
-val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
-
-
-(*i*)
-(* These are for Nbtermdn *)
-
-type term_label =
-  | GRLabel of global_reference
-  | ProdLabel
-  | LambdaLabel
-  | SortLabel of sorts option
-
-val constr_pat_discr_st : transparent_state ->
-  constr_pattern -> (term_label * constr_pattern list) option
-val constr_val_discr_st : transparent_state ->
-  constr -> (term_label * constr list) Dn.lookup_res
-
-val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option
-val constr_val_discr : constr -> (term_label * constr list) Dn.lookup_res
-
+module Make :
+  functor (Z : Map.OrderedType) ->
+sig
+  
+  type t
+    
+  type 'a lookup_res
+    
+  val create : unit -> t
+    
+  (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *)
+    
+  val add : t -> transparent_state -> (constr_pattern * Z.t) -> t
+    
+  val rmv : t -> transparent_state -> (constr_pattern * Z.t) -> t
+    
+  (* [lookup t c] looks for patterns (with their action) matching term [c] *)
+    
+  val lookup : t -> transparent_state -> constr -> (constr_pattern * Z.t) list
+    
+  val app : ((constr_pattern * Z.t) -> unit) -> t -> unit
+
+    
+  (*i*)
+  (* These are for Nbtermdn *)
+ 
+  type term_label = 
+    | GRLabel of global_reference
+    | ProdLabel 
+    | LambdaLabel
+    | SortLabel of sorts option
+	
+  val constr_pat_discr_st : transparent_state ->
+    constr_pattern -> (term_label * constr_pattern list) option
+  val constr_val_discr_st : transparent_state ->
+    constr -> (term_label * constr list) lookup_res
+    
+  val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option
+  val constr_val_discr : constr -> (term_label * constr list) lookup_res
+    
 (*i*)
+end