Enhanced discrimination nets implementation, which can now work with

goals containing existentials and use transparency information on
constants (optionally). Only used by the typeclasses eauto engine for
now, but could be used for other hint bases easily (just switch a boolean).
Had to add a new "creation" hint to be able to set said boolean upon
creation of the typeclass_instances hint db.
Improve the proof-search algorithm for Morphism, up to 10 seconds
gained in e.g. Field_theory, Ring_polynom. Added a morphism
declaration for [compose].
One needs to declare more constants as being unfoldable using
the [Typeclasses unfold] command so that discrimination is done correctly, but
that amounts to only 6 declarations in the standard library.


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

11 files changed, 382 insertions, 214 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0d5d275384..69fe51efa8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -91,18 +91,20 @@ type search_entry = stored_data list * stored_data list * stored_data Btermdn.t
 
 let empty_se = ([],[],Btermdn.create ())
 
-let add_tac t (l,l',dn) =
-  match t.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 dn (pat,t)) else (l, l', dn)
-
-
-let lookup_tacs (hdc,c) (l,l',dn) =
-  let l'  = List.map snd (Btermdn.lookup dn c) in
+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)
+
+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')
+    
+let lookup_tacs (hdc,c) st (l,l',dn) =
+  let l'  = List.map snd (Btermdn.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 
@@ -110,12 +112,18 @@ module Constr_map = Map.Make(struct
 
 module Hint_db = struct
 
-  type t = search_entry Constr_map.t
-
-  let empty = Constr_map.empty
+  type t = { 
+    hintdb_state : Names.transparent_state;
+    use_dn : bool;
+    hintdb_map : search_entry Constr_map.t
+  }
 
+  let empty use_dn = { hintdb_state = empty_transparent_state;
+		       use_dn = use_dn;
+		       hintdb_map = Constr_map.empty }
+    
   let find key db =
-    try Constr_map.find key db
+    try Constr_map.find key db.hintdb_map
     with Not_found -> empty_se
 
   let map_all k db =
@@ -123,21 +131,45 @@ module Hint_db = struct
       Sort.merge pri_order l l'
    
   let map_auto (k,c) db =
-    lookup_tacs (k,c) (find k db)
+    let st = if db.use_dn then Some db.hintdb_state else None in
+      lookup_tacs (k,c) st (find k db)
 
   let add_one (k,v) db =
-    let oval = find k db in 
-      Constr_map.add k (add_tac v oval) db
-
+    let st',rebuild =
+      match v.code with
+      | Unfold_nth egr ->
+	  let (ids,csts) = db.hintdb_state in
+	    (match egr with
+	    | EvalVarRef id -> (Idpred.add id ids, csts)
+	    | EvalConstRef cst -> (ids, Cpred.add cst csts)), true
+      | _ -> db.hintdb_state, false
+    in
+    let dnst, db = 
+      if db.use_dn then 
+	Some st', { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map }
+      else None, db
+    in
+    let oval = find k db in
+    let pat = if not db.use_dn && v.pri = 0 then None else v.pat in
+      { db with hintdb_map = Constr_map.add k (add_tac pat v dnst oval) db.hintdb_map;
+	hintdb_state = st' }
+	
   let add_list l db = List.fold_right add_one l db
+    
+  let iter f db = Constr_map.iter (fun k (l,l',_) -> f k (l@l')) db.hintdb_map
+    
+  let transparent_state db = db.hintdb_state
 
-  let iter f db = Constr_map.iter (fun k (l,l',_) -> f k (l@l')) db
+  let set_transparent_state db st = { db with hintdb_state = st }
 
+  let set_rigid db cst = 
+    let (ids,csts) = db.hintdb_state in
+      { db with hintdb_state = (ids, Cpred.remove cst csts) }
 end
 
 module Hintdbmap = Gmap
 
-type hint_db = Names.transparent_state * Hint_db.t
+type hint_db = Hint_db.t
 
 type frozen_hint_db_table = (string,hint_db) Hintdbmap.t 
 
@@ -158,7 +190,9 @@ let current_db_names () =
 (*                       Definition of the summary                        *)
 (**************************************************************************)
 
-let init     () = searchtable := Hintdbmap.empty
+let auto_init : (unit -> unit) ref = ref (fun () -> ())
+  
+let init     () = searchtable := Hintdbmap.empty; !auto_init ()
 let freeze   () = !searchtable
 let unfreeze fs = searchtable := fs
 
@@ -184,18 +218,21 @@ let try_head_pattern c =
   try head_pattern_bound c
   with BoundPattern -> error "Bound head variable"
 
+let dummy_goal = 
+  {it = make_evar empty_named_context_val mkProp;
+   sigma = empty}
+
 let make_exact_entry pri (c,cty) =
   let cty = strip_outer_cast cty in
   match kind_of_term cty with
     | Prod (_,_,_) -> 
 	failwith "make_exact_entry"
     | _ ->
+        let ce = mk_clenv_from dummy_goal (c,cty) in
+	let c' = clenv_type ce in
+	let pat = Pattern.pattern_of_constr c' in
 	(head_of_constr_reference (List.hd (head_constr cty)),
-	   { pri=(match pri with Some pri -> pri | None -> 0); pat=None; code=Give_exact c })
-
-let dummy_goal = 
-  {it = make_evar empty_named_context_val mkProp;
-   sigma = empty}
+	   { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
 
 let make_apply_entry env sigma (eapply,verbose) pri (c,cty) =
   let cty = hnf_constr env sigma cty in
@@ -279,32 +316,23 @@ open Vernacexpr
 (*               declaration of the AUTOHINT library object               *)
 (**************************************************************************)
 
-let add_hint_list hintlist (st,db) =
-  let db' = Hint_db.add_list hintlist db in
-  let st' = 
-    List.fold_left 
-      (fun (ids, csts as st) (_, hint) -> 
-	match hint.code with
-	  | Unfold_nth egr ->
-	      (match egr with
-		| EvalVarRef id -> (Idpred.add id ids, csts)
-		| EvalConstRef cst -> (ids, Cpred.add cst csts))
-	  | _ -> st)
-      st hintlist
-  in (st', db')
-
 (* If the database does not exist, it is created *)
 (* TODO: should a warning be printed in this case ?? *)
 let add_hint dbname hintlist = 
   try 
     let db = searchtable_map dbname in
-    let db' = add_hint_list hintlist db in
+    let db' = Hint_db.add_list hintlist db in
     searchtable_add (dbname,db')
   with Not_found -> 
-    let db = add_hint_list hintlist (empty_transparent_state, Hint_db.empty) in
+    let db = Hint_db.add_list hintlist (Hint_db.empty false) in
     searchtable_add (dbname,db)
 
-let cache_autohint (_,(local,name,hints)) = add_hint name hints
+type hint_action = CreateDB of bool | UpdateDB of (global_reference * pri_auto_tactic) list
+
+let cache_autohint (_,(local,name,hints)) = 
+  match hints with
+  | CreateDB b -> searchtable_add (name, Hint_db.empty b)
+  | UpdateDB hints -> add_hint name hints
 
 let forward_subst_tactic = 
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
@@ -354,12 +382,15 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
       if lab' == lab && data' == data then hint else
 	(lab',data')
   in
-  let hintlist' = list_smartmap subst_hint hintlist in
-    if hintlist' == hintlist then obj else
-      (local,name,hintlist')
-
+    match hintlist with
+    | CreateDB _ -> obj
+    | UpdateDB hintlist ->
+	let hintlist' = list_smartmap subst_hint hintlist in
+	  if hintlist' == hintlist then obj else
+	    (local,name,UpdateDB hintlist')
+	      
 let classify_autohint (_,((local,name,hintlist) as obj)) =
-  if local or hintlist = [] then Dispose else Substitute obj
+  if local or hintlist = (UpdateDB []) then Dispose else Substitute obj
 
 let export_autohint ((local,name,hintlist) as obj) =
   if local then None else Some obj
@@ -373,6 +404,9 @@ let (inAutoHint,outAutoHint) =
                     export_function = export_autohint }
 
 
+let create_hint_db l n b = 
+  Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB b))
+      
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
@@ -381,19 +415,18 @@ let add_resolves env sigma clist local dbnames =
     (fun dbname ->
        Lib.add_anonymous_leaf
 	 (inAutoHint
-	    (local,dbname,
-     	     List.flatten (List.map (fun (x, y) ->
-	       make_resolves env sigma (true,Flags.is_verbose()) x y) clist))))
+	    (local,dbname, UpdateDB
+     	      (List.flatten (List.map (fun (x, y) ->
+		make_resolves env sigma (true,Flags.is_verbose()) x y) clist)))))
     dbnames
 
 
 let add_unfolds l local dbnames =
   List.iter 
     (fun dbname -> Lib.add_anonymous_leaf 
-       (inAutoHint (local,dbname, List.map make_unfold l)))
+       (inAutoHint (local,dbname, UpdateDB (List.map make_unfold l))))
     dbnames
 
-
 let add_extern pri (patmetas,pat) tacast local dbname =
   (* We check that all metas that appear in tacast have at least
      one occurence in the left pattern pat *)
@@ -404,7 +437,7 @@ let add_extern pri (patmetas,pat) tacast local dbname =
 	  (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound")
     | []  ->
 	Lib.add_anonymous_leaf
-	  (inAutoHint(local,dbname, [make_extern pri pat tacast]))
+	  (inAutoHint(local,dbname, UpdateDB [make_extern pri pat tacast]))
 
 let add_externs pri pat tacast local dbnames = 
   List.iter (add_extern pri pat tacast local) dbnames
@@ -413,7 +446,7 @@ let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(local,dbname, List.map (make_trivial env sigma) l)))
+	 inAutoHint(local,dbname, UpdateDB (List.map (make_trivial env sigma) l))))
     dbnames
 
 let forward_intern_tac = 
@@ -493,7 +526,7 @@ let fmt_hint_list_for_head c =
   let dbs = Hintdbmap.to_list !searchtable in
   let valid_dbs = 
     map_succeed 
-      (fun (name,(_,db)) -> (name,db,Hint_db.map_all c db)) 
+      (fun (name,db) -> (name,db,Hint_db.map_all c db)) 
       dbs 
   in
   if valid_dbs = [] then 
@@ -519,11 +552,11 @@ let fmt_hint_term cl =
     let valid_dbs = 
       if occur_existential cl then 
 	map_succeed 
-	  (fun (name, (_, db)) -> (name, db, Hint_db.map_all hd db)) 
+	  (fun (name, db) -> (name, db, Hint_db.map_all hd db)) 
 	  dbs
       else 
 	map_succeed 
-	  (fun (name, (_, db)) -> 
+	  (fun (name, db) -> 
 	     (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db)) 
 	  dbs
     in 
@@ -544,7 +577,8 @@ let print_applicable_hint () =
   print_hint_term (pf_concl gl)
     
 (* displays the whole hint database db *)
-let print_hint_db ((ids, csts),db) =
+let print_hint_db db =
+  let (ids, csts) = Hint_db.transparent_state db in
   msg (hov 0
 	  (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++
 	   str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ()));
@@ -610,7 +644,7 @@ let make_local_hint_db eapply lems g =
   let sign = pf_hyps g in
   let hintlist = list_map_append (pf_apply make_resolve_hyp g) sign in
   let hintlist' = list_map_append (pf_apply make_resolves g (eapply,false) None) lems in
-    (empty_transparent_state, Hint_db.add_list hintlist' (Hint_db.add_list hintlist Hint_db.empty))
+    Hint_db.add_list hintlist' (Hint_db.add_list hintlist (Hint_db.empty false))
 
 (* Serait-ce possible de compiler d'abord la tactique puis de faire la
    substitution sans passer par bdize dont l'objectif est de préparer un
@@ -648,7 +682,7 @@ let rec trivial_fail_db mod_delta db_list local_db gl =
     tclTHEN intro 
       (fun g'->
 	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-	 in trivial_fail_db mod_delta db_list (add_hint_list hintl local_db) g')
+	 in trivial_fail_db mod_delta db_list (Hint_db.add_list hintl local_db) g')
   in
   tclFIRST 
     (assumption::intro_tac::
@@ -658,12 +692,10 @@ let rec trivial_fail_db mod_delta db_list local_db gl =
 and my_find_search_nodelta db_list local_db hdc concl =
   let tacl = 
     if occur_existential concl then 
-      list_map_append
-	(fun (st, db) -> (Hint_db.map_all hdc db))
+      list_map_append (Hint_db.map_all hdc)
 	(local_db::db_list)
     else
-      list_map_append (fun (_, db) -> 
-	Hint_db.map_auto (hdc,concl) db)
+      list_map_append (Hint_db.map_auto (hdc,concl))
       	(local_db::db_list)
   in
     List.map 
@@ -691,12 +723,13 @@ and my_find_search_delta db_list local_db hdc concl =
   let tacl = 
     if occur_existential concl then 
       list_map_append
-	(fun (st, db) -> 
-	  let st = {flags with modulo_delta = st} in
+	(fun db -> 
+	  let st = {flags with modulo_delta = Hint_db.transparent_state db} in
 	    List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
 	(local_db::db_list)
     else
-      list_map_append (fun ((ids, csts as st), db) -> 
+      list_map_append (fun db -> 
+	let (ids, csts as st) = Hint_db.transparent_state db in
 	let st, l = 
 	  let l =
 	    if (Idpred.is_empty ids && Cpred.is_empty csts)
@@ -817,7 +850,7 @@ let rec search_gen decomp n mod_delta db_list local_db extra_sign goal =
 		(mkVar hid, htyp)]
 	   with Failure _ -> [] 
 	 in
-         search_gen decomp n mod_delta db_list (add_hint_list hintl local_db) [d] g') 
+         search_gen decomp n mod_delta db_list (Hint_db.add_list hintl local_db) [d] g') 
   in
   let rec_tacs = 
     List.map 
@@ -956,7 +989,7 @@ let rec super_search n db_list local_db argl goal =
      (tclTHEN intro 
         (fun g -> 
 	   let hintl = pf_apply make_resolve_any_hyp g (pf_last_hyp g) in
-	   super_search n db_list (add_hint_list hintl local_db)
+	   super_search n db_list (Hint_db.add_list hintl local_db)
 	     argl g))
      ::
      ((List.map 
@@ -974,7 +1007,7 @@ let search_superauto n to_add argl g =
       (fun (id,c) -> add_named_decl (id, None, pf_type_of g c))
       to_add empty_named_context in
   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
-  let db = add_hint_list db0 (make_local_hint_db false [] g) in
+  let db = Hint_db.add_list db0 (make_local_hint_db false [] g) in
   super_search n [Hintdbmap.find "core" !searchtable] db argl g
 
 let superauto n to_add argl  = 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 5b151162c4..c5df28d427 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -47,24 +47,30 @@ type search_entry = stored_data list * stored_data list * stored_data Btermdn.t
 module Hint_db :
   sig
     type t
-    val empty : t
+    val empty : bool -> t
     val find : global_reference -> t -> search_entry
     val map_all : global_reference -> t -> pri_auto_tactic list
     val map_auto : global_reference * constr -> t -> pri_auto_tactic list
     val add_one : global_reference * pri_auto_tactic -> t -> t
     val add_list : (global_reference * pri_auto_tactic) list -> t -> t
     val iter : (global_reference -> stored_data list -> unit) -> t -> unit
+
+    val transparent_state : t -> transparent_state
+    val set_transparent_state : t -> transparent_state -> t
+    val set_rigid : t -> constant -> t
   end
 
 type hint_db_name = string
 
-type hint_db = transparent_state * Hint_db.t
+type hint_db = Hint_db.t
 
 val searchtable_map : hint_db_name -> hint_db
 
-val current_db_names : unit -> hint_db_name list
+val searchtable_add : (hint_db_name * hint_db) -> unit
 
-val add_hint_list : (global_reference * pri_auto_tactic) list -> hint_db -> hint_db
+val create_hint_db : bool -> hint_db_name -> bool -> unit
+
+val current_db_names : unit -> hint_db_name list
 
 val add_hints : locality_flag -> hint_db_name list -> hints -> unit
 
@@ -207,3 +213,5 @@ val superauto : int -> (identifier * constr) list -> autoArguments list -> tacti
 *)
 
 val h_superauto : int option -> reference list -> bool -> bool -> tactic
+
+val auto_init : (unit -> unit) ref
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 7d41ebf9df..2412968a1e 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -9,6 +9,7 @@
 (* $Id$ *)
 
 open Term
+open Names
 open Termdn
 open Pattern
 open Libnames
@@ -19,6 +20,23 @@ 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
+
 let bounded_constr_pat_discr (t,depth) =
   if depth = 0 then 
     None 
@@ -29,24 +47,44 @@ let bounded_constr_pat_discr (t,depth) =
 	    
 let bounded_constr_val_discr (t,depth) =
   if depth = 0 then 
-    None 
+    Dn.Nothing 
   else
     match constr_val_discr t with
-      | None -> None
-      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+      | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
+      | Dn.Nothing -> Dn.Nothing
+      | Dn.Everything -> Dn.Nothing
 
 type 'a t = (global_reference,constr_pattern * int,'a) Dn.t
-
+  
 let create = Dn.create
+  
+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 add dn (c,v) = Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)
-
-let rmv dn (c,v) = Dn.rmv dn bounded_constr_pat_discr ((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 dn t =
-  List.map 
-    (fun ((c,_),v) -> (c,v)) 
-    (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))
+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
 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index e0ba8ddcaf..86107641d0 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -11,6 +11,7 @@
 (*i*)
 open Term
 open Pattern
+open Names
 (*i*)
 
 (* Discrimination nets with bounded depth. *)
@@ -19,10 +20,10 @@ type 'a t
 
 val create : unit -> 'a t
 
-val add : 'a t -> (constr_pattern * 'a) -> 'a t
-val rmv : 'a t -> (constr_pattern * 'a) -> 'a t
-
-val lookup : 'a t -> constr -> (constr_pattern * 'a) list
+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 dnet_depth : int ref
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a353a4222f..68cf37b49e 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -43,6 +43,8 @@ open Evd
 let default_eauto_depth = 100
 let typeclasses_db = "typeclass_instances"
 
+let _ = Auto.auto_init := (fun () -> Auto.create_hint_db false typeclasses_db true)
+
 let check_imported_library d =
   let d' = List.map id_of_string d in
   let dir = make_dirpath (List.rev d') in
@@ -98,7 +100,7 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
-	     (add_hint_list hintl local_db) g'))) ::
+	      (Hint_db.add_list hintl local_db) g'))) ::
     (List.map pi1 (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
@@ -106,13 +108,17 @@ let rec e_trivial_fail_db db_list local_db goal =
 and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
   let hintl =
-    if occur_existential concl then
+(*     if occur_existential concl then *)
+(*       list_map_append *)
+(* 	(fun db -> *)
+(* 	  let st = Hint_db.transparent_state db in *)
+(* 	    List.map (fun x -> (st, x)) (Hint_db.map_all hdc db)) *)
+(* 	(local_db::db_list) *)
+(*     else *)
       list_map_append
-	(fun (st, db) -> List.map (fun x -> (st, x)) (Hint_db.map_all hdc db))
-	(local_db::db_list)
-    else
-      list_map_append
-	(fun (st, db) -> List.map (fun x -> (st, x)) (Hint_db.map_auto (hdc,concl) db))
+	(fun db -> 
+	  let st = Hint_db.transparent_state db in
+	    List.map (fun x -> (st, x)) (Hint_db.map_auto (hdc,concl) db))
 	(local_db::db_list)
   in 
   let tac_of_hint = 
@@ -186,6 +192,8 @@ module SearchProblem = struct
 (*       (let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (*       let evars = Evarutil.nf_evars (Refiner.project glls) in *)
 (*     	msg (str"Goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n")); *)
+    let glls,nv = apply_tac_list tclNORMEVAR glls in
+    let v p = v (nv p) in
     let rec aux = function
       | [] -> []
       | (tac,pri,pptac) :: tacl -> 
@@ -214,7 +222,7 @@ module SearchProblem = struct
       List.length (sig_it (fst s.tacres)) + 
 	nb_empty_evars (sig_sig (fst s.tacres))
     in
-      if d <> 0 && d <> 1 then d else
+      if d <> 0 then d else
 	let pri = s.pri - s'.pri in
 	  if pri <> 0 then pri
 	  else nbgoals s - nbgoals s'
@@ -239,24 +247,26 @@ module SearchProblem = struct
 	  List.map (fun (res,pri,pp) -> { s with tacres = res; pri = 0;
 	    last_tactic = pp; localdb = List.tl s.localdb }) l
       in
-(*       let intro_tac =  *)
-(* 	List.map  *)
-(* 	  (fun ((lgls,_) as res,pri,pp) ->  *)
-(* 	     let g' = first_goal lgls in  *)
-(* 	     let hintl =  *)
-(* 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') *)
-(* 	     in	        *)
-(*              let ldb = Hint_db.add_list hintl (match s.localdb with [] -> assert false | hd :: _ -> hd) in *)
-(* 	       { s with tacres = res;  *)
-(* 		 last_tactic = pp; *)
-(* 		 pri = pri; *)
-(* 		 localdb = ldb :: List.tl s.localdb }) *)
-(* 	  (filter_tactics s.tacres [Tactics.intro,1,(str "intro")]) *)
-(*       in *)
+      let intro_tac =
+	List.map
+	  (fun ((lgls,_) as res,pri,pp) ->
+	     let g' = first_goal lgls in
+	     let hintl =
+	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	     in
+             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
+	       { s with tacres = res;
+		 last_tactic = pp;
+		 pri = pri;
+		 localdb = ldb :: List.tl s.localdb })
+	  (filter_tactics s.tacres [Tactics.intro,1,(str "intro")])
+      in
       let possible_resolve ((lgls,_) as res, pri, pp) =
 	let nbgl' = List.length (sig_it lgls) in
 	  if nbgl' < nbgl then
-	    { s with tacres = res; last_tactic = pp; pri = pri;
+	    { s with 
+	      depth = pred s.depth;
+	      tacres = res; last_tactic = pp; pri = pri;
 	      localdb = List.tl s.localdb }
 	  else 
 	    { s with 
@@ -265,13 +275,14 @@ module SearchProblem = struct
 	      localdb = 
 		list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }
       in
+      let concl = Evarutil.nf_evar (project g) (pf_concl g) in
       let rec_tacs = 
 	let l = 
-	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) concl)
 	in
 	List.map possible_resolve l
       in
-      List.sort compare (assumption_tacs (* @intro_tac  @ custom_tac *) @ rec_tacs)
+      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
 
   let pp s = 
     msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ 
@@ -342,9 +353,11 @@ let e_breadth_search debug s =
     in let s = tac s in s.tacres
   with Not_found -> error "EAuto: breadth first search failed"
 
-let e_search_auto debug (in_depth,p) lems db_list gls = 
+let e_search_auto debug (in_depth,p) lems st db_list gls = 
   let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in
-  let local_dbs = List.map (fun gl -> make_local_hint_db true lems ({it = gl; sigma = sigma})) gls' in
+  let local_dbs = List.map (fun gl -> 
+    let db = make_local_hint_db true lems ({it = gl; sigma = sigma}) in
+      Hint_db.set_transparent_state db st) gls' in
   let state = make_initial_state p gls db_list local_dbs in
   if in_depth then 
     e_depth_search debug state
@@ -355,20 +368,14 @@ let full_eauto debug n lems gls =
   let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
-    e_search_auto debug n lems db_list gls
+    e_search_auto debug n lems empty_transparent_state db_list gls
 
 let nf_goal (gl, valid) =
   { gl with sigma = Evarutil.nf_evars gl.sigma }, valid
 
 let typeclasses_eauto debug n lems gls =
-  let dbnames = [typeclasses_db] in
-  let db_list = List.map
-    (fun x -> 
-      try searchtable_map x 
-      with Not_found -> (empty_transparent_state, Hint_db.empty))
-    dbnames 
-  in
-    e_search_auto debug n lems db_list gls
+  let db = searchtable_map typeclasses_db in
+    e_search_auto debug n lems (Hint_db.transparent_state db) [db] gls
 
 exception Found of evar_map
 
@@ -505,6 +512,20 @@ VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
   ]
 END
 
+VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings
+| [ "Typeclasses" "rigid" reference_list(cl) ] -> [
+    let db = searchtable_map typeclasses_db in
+    let db' = 
+      List.fold_left (fun acc r -> 
+	let gr = Syntax_def.global_with_alias r in
+	  match gr with
+	  | ConstRef c -> Hint_db.set_rigid acc c 
+	  | _ -> acc) db cl
+    in
+      searchtable_add (typeclasses_db,db')
+ ]
+END
+
 (** Typeclass-based rewriting. *)
 
 let respect_proj = lazy (mkConst (snd (List.hd (Lazy.force morphism_class).cl_projs)))
@@ -539,7 +560,7 @@ let coq_inverse = lazy (gen_constant (* ["Classes"; "RelationClasses"] "inverse"
 let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |])
 
 let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement")
-let pointwise_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "pointwise_relation")
+let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation")
 
 let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep")
 let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
@@ -780,11 +801,12 @@ let unify_eqn env sigma hypinfo t =
 		let mvs = clenv_dependent false env' in
 		  clenv_pose_metas_as_evars env' mvs
 	      in
-	      let c1 = Clenv.clenv_nf_meta env' c1 
-	      and c2 = Clenv.clenv_nf_meta env' c2
-	      and car = Clenv.clenv_nf_meta env' car
-	      and rel = Clenv.clenv_nf_meta env' rel in
-	      let prf = Clenv.clenv_value env' in
+	      let evd' = Typeclasses.resolve_typeclasses env'.env env'.evd in
+	      let env' = { env' with evd = evd' } in
+	      let nf c = Evarutil.nf_evar (Evd.evars_of evd') (Clenv.clenv_nf_meta env' c) in
+	      let c1 = nf c1 and c2 = nf c2
+	      and car = nf car and rel = nf rel 
+	      and prf = nf (Clenv.clenv_value env') in
 	      let ty1 = Typing.mtype_of env'.env env'.evd c1 
 	      and ty2 = Typing.mtype_of env'.env env'.evd c2
 	      in
@@ -1057,11 +1079,17 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
   try cl_rewrite_clause_aux ~flags hypinfo goal_meta occs clause gl
   with DependentMorphism -> tclFAIL 0 (str " setoid rewrite failed: cannot handle dependent morphisms") gl
 
-let cl_rewrite_clause c left2right occs clause gl =
+let cl_rewrite_clause (evm,c) left2right occs clause gl =
   init_setoid ();
   let meta = Evarutil.new_meta() in
   let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in
-  let hypinfo = ref (decompose_setoid_eqhyp (pf_env gl) (project gl) c left2right) in
+  let env = pf_env gl in
+  let evars = Evd.merge (project gl) evm in
+(*   let c = *)
+(*     let j = Pretyping.Default.understand_judgment_tcc evars env c in *)
+(*       j.Environ.uj_val *)
+(*   in *)
+  let hypinfo = ref (decompose_setoid_eqhyp env evars c left2right) in
     cl_rewrite_clause_aux hypinfo meta occs clause gl
 
 open Genarg
@@ -1075,16 +1103,16 @@ let occurrences_of = function
       (true,nl)
 
 TACTIC EXTEND class_rewrite
-| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ]
-| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o all_occurrences None ]
+| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) open_constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ]
+| [ "clrewrite" orient(o) open_constr(c) ] -> [ cl_rewrite_clause c o all_occurrences None ]
 END
 
 
 let clsubstitute o c =
-  let is_tac id = match kind_of_term c with Var id' when id' = id -> true | _ -> false in
+  let is_tac id = match kind_of_term (snd c) with Var id' when id' = id -> true | _ -> false in
     Tacticals.onAllClauses 
       (fun cl -> 
 	match cl with
@@ -1092,7 +1120,7 @@ let clsubstitute o c =
 	  | _ -> tclTRY (cl_rewrite_clause c o all_occurrences cl))
 
 TACTIC EXTEND substitute
-| [ "substitute" orient(o) constr(c) ] -> [ clsubstitute o c ]
+| [ "substitute" orient(o) open_constr(c) ] -> [ clsubstitute o c ]
 END
 
 let pr_debug _prc _prlc _prt b =
@@ -1146,7 +1174,8 @@ TACTIC EXTEND typeclasses_eauto
       fun gl -> 
 	let gls = {it = [sig_it gl]; sigma = project gl} in
 	let vals v = List.hd v in
-	  typeclasses_eauto d (mode, depth) [] (gls, vals) ]
+	  try typeclasses_eauto d (mode, depth) [] (gls, vals) 
+	  with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl ]
 END
 
 
@@ -1172,15 +1201,15 @@ let _ =
 (* Compatibility with old Setoids *)
   
 TACTIC EXTEND setoid_rewrite
-   [ "setoid_rewrite" orient(o) constr(c) ]
+   [ "setoid_rewrite" orient(o) open_constr(c) ]
    -> [ cl_rewrite_clause c o all_occurrences None ]
- | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) ] ->
+ | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) ] ->
       [ cl_rewrite_clause c o all_occurrences (Some (([],id), []))]
- | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) ] ->
+ | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) ] ->
       [ cl_rewrite_clause c o (occurrences_of occ) None]
- | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id)] ->
+ | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id)] ->
       [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))]
- | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ)] ->
+ | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ)] ->
       [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))]
 END
 
@@ -1690,3 +1719,16 @@ TACTIC EXTEND apply_typeclasses
 	     Clenvtac.clenv_refine true {cl' with evd = evd'} gl) gl
    ]
 END
+
+(* TACTIC EXTEND solve_evar *)
+(*   [ "solve_evar" int_or_var(n) ] -> [ fun gl -> *)
+(*     let n = match n with ArgArg i -> pred i | _ -> assert false in *)
+(*     let ev, evi = try List.nth (Evd.to_list (project gl)) n with Not_found -> assert false in *)
+(*     let id = pf_get_new_id (add_suffix (id_of_string "evar") (string_of_int n)) gl in *)
+(*       tclTHEN (true_cut (Name id) evi.evar_concl gl) *)
+	
+(*   ] *)
+(* END *)
+
+
+(*      let nprod = nb_prod (pf_concl gl) in *)
diff --git a/tactics/dn.ml b/tactics/dn.ml
index dbfafcd61c..0809c80ebb 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -1,3 +1,4 @@
+(* -*- 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 *)
@@ -32,6 +33,10 @@
 
 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
@@ -46,29 +51,44 @@ let path_of dna =
 	    
   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)
+    | 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] with Not_found -> []
-
+  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 =
-    (tm_of tm None)@
-    (match dna t with
-       | None -> []
-       | Some(lbl,v) ->
-	   List.fold_left 
-	     (fun l c -> List.flatten(List.map (lookrec c) l))
-             (tm_of tm (Some(lbl,List.length v))) v)
+    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 Tlm.xtract (lookrec t tm))
+    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))
diff --git a/tactics/dn.mli b/tactics/dn.mli
index e07742e0fd..e37ed9af3f 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -28,13 +28,19 @@ val add : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf
 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
+
 (* [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) decompose_fun -> 'term
+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
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 3b982b4c08..70bc9a5924 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -111,7 +111,7 @@ let rec e_trivial_fail_db mod_delta db_list local_db goal =
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db mod_delta db_list
-	     (add_hint_list hintl local_db) g'))) ::
+	      (Hint_db.add_list hintl local_db) g'))) ::
     (List.map fst (e_trivial_resolve mod_delta db_list local_db (pf_concl goal)) )
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
@@ -124,10 +124,9 @@ and e_my_find_search_nodelta db_list local_db hdc concl =
   let hdc = head_of_constr_reference hdc in
   let hintl =
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> Hint_db.map_all hdc db) (local_db::db_list)
+      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> 
-	Hint_db.map_auto (hdc,concl) db) (local_db::db_list)
+      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
   in 
   let tac_of_hint = 
     fun {pri=b; pat = p; code=t} -> 
@@ -160,12 +159,12 @@ and e_my_find_search_delta db_list local_db hdc concl =
   let hdc = head_of_constr_reference hdc in
   let hintl =
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> 
-	let flags = {auto_unif_flags with modulo_delta = st} in
+      list_map_append (fun db -> 
+	let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
 	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> 
-	let flags = {auto_unif_flags with modulo_delta = st} in
+      list_map_append (fun db -> 
+	let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
 	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in 
   let tac_of_hint = 
@@ -285,8 +284,7 @@ module SearchProblem = struct
 	     let hintl = 
 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 	     in
-	       
-             let ldb = add_hint_list hintl (List.hd s.localdb) in
+             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
 	     { depth = s.depth; tacres = res; 
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb })
@@ -452,7 +450,8 @@ let autosimpl db cl =
     else []
   in
   let unfolds = List.concat (List.map (fun dbname -> 
-    let ((ids, csts), _) = searchtable_map dbname in
+    let db = searchtable_map dbname in
+    let (ids, csts) = Hint_db.transparent_state db in
       unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @
       unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
   in unfold_option unfolds cl
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index c53a5088a9..431748868c 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -46,14 +46,14 @@ let add dn (na,(pat,valu)) =
   let hkey = Option.map fst (Termdn.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 (get_dn dnm hkey) (pat,valu)) dnm
+  dn.patterns <- Gmap.add hkey (Btermdn.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 
   dn.table <- Gmap.remove na dn.table;
   let dnm = dn.patterns in
-  dn.patterns <- Gmap.add hkey (Btermdn.rmv (get_dn dnm hkey) (pat,valu)) dnm
+  dn.patterns <- Gmap.add hkey (Btermdn.rmv None (get_dn dnm hkey) (pat,valu)) dnm
 
 let in_dn dn na = Gmap.mem na dn.table
 			  
@@ -62,8 +62,12 @@ let remap ndn na (pat,valu) =
   add ndn (na,(pat,valu))
 
 let lookup dn valu =
-  let hkey = Option.map fst (Termdn.constr_val_discr valu) in 
-  try Btermdn.lookup (Gmap.find hkey  dn.patterns) valu with Not_found -> []
+  let hkey = 
+    match (Termdn.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 -> []
 
 let app f dn = Gmap.iter f dn.table
 		       
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 1c95f7fdc6..995183dc90 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -41,43 +41,53 @@ let decomp_pat =
   decrec []   
 
 let constr_pat_discr t =
-  if not (occur_meta_pattern t) then 
+  if not (occur_meta_pattern t) then
     None
   else
     match decomp_pat t with
-      | PRef ((IndRef _) as ref), args
-      | PRef ((ConstructRef _ ) as ref), args
-      | PRef ((VarRef _) as ref), args -> Some(ref,args)
-      | _ -> None
-
-let constr_val_discr t =
-  let c, l = decomp t in
-  match kind_of_term c with
-    (* Const _,_) -> Some(TERM c,l) *)
-    | Ind ind_sp -> Some(IndRef ind_sp,l)
-    | Construct cstr_sp -> Some(ConstructRef cstr_sp,l)
-    | Var id -> Some(VarRef id,l)
+    | PRef ((IndRef _) as ref), args
+    | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args)
+    | PRef ((VarRef v) as ref), args -> Some(ref,args)
     | _ -> None
 
-(* Les deux fonctions suivantes ecrasaient les precedentes, 
-   ajout d'un suffixe _nil CP 16/08 *) 
-
-let constr_pat_discr_nil t =
-  match constr_pat_discr t with
-    | None -> None
-    | Some (c,_) -> Some(c,[])
-
-let constr_val_discr_nil t =
-  match constr_val_discr t with
-    | None -> None
-    | Some (c,_) -> Some(c,[])
+let constr_pat_discr_st (idpred,cpred) t =
+  match decomp_pat t with
+  | PRef ((IndRef _) as ref), args
+  | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args)
+  | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) -> 
+      Some(ref,args)
+  | PVar v, args when not (Idpred.mem v idpred) ->
+      Some(VarRef v,args)
+  | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
+      Some (ref, args)
+  | _ -> None
+
+open Dn
+
+let constr_val_discr t =  
+  let c, l = decomp t in
+    match kind_of_term c with
+    | Ind ind_sp -> Label(IndRef ind_sp,l)
+    | Construct cstr_sp -> Label((ConstructRef cstr_sp),l)
+    | Var id -> Label(VarRef id,l)
+    | _ -> 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 Everything else Label(ConstRef c,l)
+    | Ind ind_sp -> Label(IndRef ind_sp,l)
+    | Construct cstr_sp -> Label((ConstructRef cstr_sp),l)
+    | Var id when not (Idpred.mem id idpred) -> Label(VarRef id,l)
+    | Evar _ -> Everything
+    | _ -> Nothing
 
 let create = Dn.create 
 
-let add dn = Dn.add dn constr_pat_discr
-
-let rmv dn = Dn.rmv dn constr_pat_discr
+let add dn st = Dn.add dn (constr_pat_discr_st st)
 
-let lookup dn t = Dn.lookup dn constr_val_discr t
+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
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 6e1bdd87ca..a9f11b3afa 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -12,6 +12,7 @@
 open Term
 open Pattern
 open Libnames
+open Names
 (*i*)
   
 (* Discrimination nets of terms. *)
@@ -22,7 +23,10 @@ open Libnames
 order in such a way patterns having the same prefix have this common
 prefix shared and the seek for the action associated to the patterns
 that a term matches are found in time proportional to the maximal
-number of nodes of the patterns matching the term *)
+number of nodes of the patterns matching the term. The [transparent_state] 
+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
 
@@ -30,13 +34,13 @@ val create : unit -> 'a t
 
 (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *)
 
-val add : 'a t -> (constr_pattern * 'a) -> 'a t
+val add : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t
 
-val rmv : 'a t -> (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 -> constr -> (constr_pattern * 'a) list
+val lookup : 'a t -> transparent_state -> constr -> (constr_pattern * 'a) list
 
 val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
 
@@ -44,9 +48,12 @@ val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
 (*i*)
 (* These are for Nbtermdn *)
 
-val constr_pat_discr : 
+val constr_pat_discr_st : transparent_state ->
   constr_pattern -> (global_reference * constr_pattern list) option
-val constr_val_discr :
-  constr -> (global_reference * constr list) option
+val constr_val_discr_st : transparent_state ->
+  constr -> (global_reference * constr list) Dn.lookup_res
+
+val constr_pat_discr : constr_pattern -> (global_reference * constr_pattern list) option
+val constr_val_discr : constr -> (global_reference * constr list) Dn.lookup_res
 
 (*i*)