This big commit addresses two problems:

  1- Management of the name-space in a modular development / sharing of non-logical objects.
  2- Performance of atomic module operations (adding a module to the environment, subtyping ...).

1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P

Module M := P.

Module M.
 Include P.
 ...
End M.

Declare Module K : S with Module M := P.

In this 3 cases we don't want to be bothered by the duplication of names. 
Of course, M.foo delta reduce to P.foo but many non-logical features of coq 
do not work modulo conversion (they use eq_constr or constr_pat object). 
To engender a transparent name-space (ie using P.foo or M.foo is the same thing) 
we quotient the name-space by the equivalence relation on names induced by the 
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of 
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo). 
So:
*************************************************************************************
*  Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values   *
*************************************************************************************

Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free 
(also for a posteriori declaration of them, ex: a notation on M.foo will be 
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.


2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based 
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate 
several functors then we have bigger vo.


Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7

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