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

27 files changed, 491 insertions, 318 deletions

diff --git a/contrib/firstorder/sequent.ml b/contrib/firstorder/sequent.ml
index e540058f1..fd5972fb7 100644
--- a/contrib/firstorder/sequent.ml
+++ b/contrib/firstorder/sequent.ml
@@ -281,7 +281,7 @@ let create_with_auto_hints l depth gl=
 	searchtable_map dbname
       with Not_found-> 
 	error ("Firstorder: "^dbname^" : No such Hint database") in
-      Hint_db.iter g (snd hdb) in
+      Hint_db.iter g hdb in
     List.iter h l;
     !seqref
 
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 3d80bd004..d7bcde69c 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 				      false
 				      (true,5)
 				      [Lazy.force refl_equal]
-				      [empty_transparent_state, Auto.Hint_db.empty]
+				      [Auto.Hint_db.empty false]
 				  )
 			   )
 			)
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 6ec0fac42..767a7dd66 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -161,21 +161,22 @@ 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 fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
 
 and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
-  let flags = Auto.auto_unif_flags in
   let hintl =
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x))
-	(Hint_db.map_all hdc db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.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) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) 
-	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.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 = 
     fun (st, ({pri=b; pat = p; code=t} as _patac)) -> 
@@ -279,7 +280,7 @@ module MySearchProblem = 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 })
@@ -375,7 +376,7 @@ let rec trivial_fail_db 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 db_list (add_hint_list hintl local_db) g')
+	 in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
   in
   tclFIRST 
     (assumption::intro_tac::
@@ -383,14 +384,15 @@ let rec trivial_fail_db db_list local_db gl =
 	(trivial_resolve db_list local_db (pf_concl gl)))) gl
 
 and my_find_search db_list local_db hdc concl =
-  let flags = Auto.auto_unif_flags in
   let tacl = 
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) 
-	(Hint_db.map_all hdc db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.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) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
-	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.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
   List.map 
     (fun (st, {pri=b; pat=p; code=t} as _patac) -> 
@@ -477,7 +479,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   with Failure _ -> [] 
 	 in
          (free_try
-	  (search_gen decomp n db_list (add_hint_list hintl local_db) [d])
+	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
 	  g'))
   in
   let rec_tacs = 
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 474b3616a..70087b2d4 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -452,11 +452,14 @@ let (theory_to_obj, obj_to_theory) =
 
 
 let setoid_of_relation env a r =
-  lapp coq_mk_Setoid
-    [|a ; r ; 
-      Class_tactics.reflexive_proof env a r ; 
-      Class_tactics.symmetric_proof env a r ; 
-      Class_tactics.transitive_proof env a r |]
+  try 
+    lapp coq_mk_Setoid
+      [|a ; r ; 
+	Class_tactics.reflexive_proof env a r ; 
+	Class_tactics.symmetric_proof env a r ; 
+	Class_tactics.transitive_proof env a r |]
+  with Not_found ->
+    error "cannot find setoid relation"
 
 let op_morph r add mul opp req m1 m2 m3 =
   lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0d5d27538..69fe51efa 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 5b151162c..c5df28d42 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 7d41ebf9d..2412968a1 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 e0ba8ddca..86107641d 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 a353a4222..68cf37b49 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 dbfafcd61..0809c80eb 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 e07742e0f..e37ed9af3 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 3b982b4c0..70bc9a592 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 c53a5088a..431748868 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 1c95f7fdc..995183dc9 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 6e1bdd87c..a9f11b3af 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*)
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 42961baea..d77704c12 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -134,8 +134,8 @@ End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance pointwise_equivalence [ Equivalence A eqA ] :
-  Equivalence (B -> A) (pointwise_relation eqA) | 9.
+Program Instance pointwise_equivalence [ Equivalence B eqB ] :
+  Equivalence (A -> B) (pointwise_relation eqB) | 9.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 05167bdc5..724021799 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -39,10 +39,6 @@ Class Morphism A (R : relation A) (m : A) : Prop :=
 
 Implicit Arguments Morphism [A].
 
-(** We allow to unfold the [relation] definition while doing morphism search. *)
-
-Typeclasses unfold relation.
-
 (** Respectful morphisms. *)
 
 (** The fully dependent version, not used yet. *)
@@ -79,6 +75,15 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
 
 Open Local Scope signature_scope.
 
+(** Pointwise lifting is just respect with leibnize equality on the left. *)
+
+Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
+  fun f g => forall x : A, R (f x) (g x).
+
+Lemma pointwise_pointwise A B (R : relation B) : 
+  relation_equivalence (pointwise_relation R) (@eq A ==> R).
+Proof. intros. split. simpl_relation. firstorder. Qed.
+
 (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
 
@@ -99,17 +104,18 @@ Proof. firstorder. Qed.
 
 (** The subrelation property goes through products as usual. *)
 
-Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] :
-  ! subrelation (B -> A) (R ==> R₁) (R ==> R₂).
-Proof. firstorder. Qed.
+Instance morphisms_subrelation_respectful [ subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂ ] :
+  subrelation (R₁ ==> S₁) (R₂ ==> S₂).
+Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 
-Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] :
-  ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
-Proof. firstorder. Qed.
+(** And of course it is reflexive. *)
+
+Instance morphisms_subrelation_refl : ! subrelation A R R | 10.
+Proof. simpl_relation. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
 
-Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m.
+Lemma subrelation_morphism [ mor : Morphism A R₁ m, sub : subrelation A R₁ R₂ ] : Morphism R₂ m.
 Proof.
   intros. apply sub. apply mor.
 Qed.
@@ -121,8 +127,9 @@ Proof. reduce. subst. firstorder. Qed.
 (** We use an external tactic to manage the application of subrelation, which is otherwise
    always applicable. We allow its use only once per branch. *)
 
-Inductive subrelation_done : Prop :=
-  did_subrelation : subrelation_done.
+Inductive subrelation_done : Prop := did_subrelation : subrelation_done.
+
+Inductive normalization_done : Prop := did_normalization.
 
 Ltac subrelation_tac := 
   match goal with
@@ -131,7 +138,7 @@ Ltac subrelation_tac :=
       set(H:=did_subrelation) ; eapply @subrelation_morphism
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
+Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
@@ -181,20 +188,10 @@ Program Instance trans_contra_co_morphism
     transitivity x0...
   Qed.
 
-(* (** Dually... *) *)
-
-(* Program Instance [ Transitive A R ] => *)
-(*   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. *)
-  
-(*   Next Obligation. *)
-(*   Proof with auto. *)
-(*     apply* trans_contra_co_morphism ; eauto. eauto. *)
-(*   Qed. *)
-
 (** Morphism declarations for partial applications. *)
 
 Program Instance trans_contra_inv_impl_morphism
-  [ Transitive A R ] : Morphism (R --> inverse impl) (R x).
+  [ Transitive A R ] : Morphism (R --> inverse impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -202,7 +199,7 @@ Program Instance trans_contra_inv_impl_morphism
   Qed.
 
 Program Instance trans_co_impl_morphism
-  [ Transitive A R ] : Morphism (R ==> impl) (R x).
+  [ Transitive A R ] : Morphism (R ==> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -210,23 +207,23 @@ Program Instance trans_co_impl_morphism
   Qed.
 
 Program Instance trans_sym_co_inv_impl_morphism
-  [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x).
+  [ PER A R ] : Morphism (R ==> inverse impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
-    transitivity y...
+    transitivity y... symmetry...
   Qed.
 
 Program Instance trans_sym_contra_impl_morphism
-  [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x).
+  [ PER A R ] : Morphism (R --> impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
-    transitivity x0...
+    transitivity x0... symmetry...
   Qed.
 
 Program Instance equivalence_partial_app_morphism
-  [ Equivalence A R ] : Morphism (R ==> iff) (R x).
+  [ Equivalence A R ] : Morphism (R ==> iff) (R x) | 1.
 
   Next Obligation.
   Proof with auto.
@@ -240,36 +237,16 @@ Program Instance equivalence_partial_app_morphism
    to get an [R y z] goal. *)
 
 Program Instance trans_co_eq_inv_impl_morphism
-  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R.
+  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-(* Program Instance [ Transitive A R ] =>  *)
-(*   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. *)
-
-(*   Next Obligation. *)
-(*   Proof with auto. *)
-(*     transitivity x... *)
-(*   Qed. *)
-
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance trans_sym_morphism
-  [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R.
-
-  Next Obligation.
-  Proof with auto.
-    split ; intros.
-    transitivity x0... transitivity x...
-  
-    transitivity y... transitivity y0... 
-  Qed.
-
-Program Instance equiv_morphism [ Equivalence A R ] :
-  Morphism (R ==> R ==> iff) R.
+Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1.
 
   Next Obligation.
   Proof with auto.
@@ -293,6 +270,15 @@ Program Instance iff_impl_id :
 Program Instance inverse_iff_impl_id :
   Morphism (iff --> impl) id.
   
+Program Instance compose_morphism A B C R₀ R₁ R₂ :
+  Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
+
+  Next Obligation.
+  Proof.
+    simpl_relation.
+    unfold compose. apply H. apply H0. apply H1.
+  Qed.
+
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
@@ -342,10 +328,6 @@ Instance morphism_morphism_proxy
   [ Morphism A R x ] : MorphismProxy A R x | 2.
 Proof. firstorder. Qed.
 
-(* Instance (A : Type) [ Reflexive B R ] => *)
-(*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
-(* Proof. simpl_relation. Qed. *)
-
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
 Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] :
@@ -373,12 +355,11 @@ Ltac partial_application_tactic :=
     end
   in
   match goal with
+    | [ _ : subrelation_done |- _ ] => fail 1
+    | [ _ : normalization_done |- _ ] => fail 1      
     | [ |- @Morphism _ _ ?m ] => on_morphism m
   end.
 
-(* Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) => *)
-(*   reflexive_partial_app_morphism : Morphism R' (m x). *)
-
 Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
@@ -406,8 +387,8 @@ Proof. firstorder. Qed.
 
 Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] :
   Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
-Proof. red ; intros.  
-  pose normalizes as r.
+Proof. red ; intros. 
+  assert(r:=normalizes).
   setoid_rewrite r.
   setoid_rewrite inverse_respectful.
   reflexivity.
@@ -415,8 +396,14 @@ Qed.
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)
 
-Program Instance morphism_inverse_morphism
-  [ Morphism A R m ] : Morphism (inverse R) m | 2.
+Definition morphism_inverse_morphism [ mor : Morphism A R m ] : Morphism (inverse R) m := mor.
+
+Ltac morphism_inverse :=
+  match goal with
+    [ |- @Morphism _ (flip _) _ ] => eapply @morphism_inverse_morphism
+  end.
+
+Hint Extern 2 (@Morphism _ _ _) => morphism_inverse : typeclass_instances.
 
 (** Bootstrap !!! *)
 
@@ -441,10 +428,9 @@ Proof.
   assumption.
 Qed.
 
-Inductive normalization_done : Prop := did_normalization.
-
 Ltac morphism_normalization := 
   match goal with
+    | [ _ : subrelation_done |- _ ] => fail 1
     | [ _ : normalization_done |- _ ] => fail 1
     | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
       set(H:=did_normalization) ; eapply @morphism_releq_morphism
@@ -465,4 +451,4 @@ Ltac morphism_reflexive :=
     | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
+Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 7dc1f95ef..ec62e12ec 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -29,7 +29,7 @@ Program Instance not_iff_morphism :
 
 (** Logical conjunction. *)
 
-Program Instance and_impl_iff_morphism :
+Program Instance and_impl_morphism :
   Morphism (impl ==> impl ==> impl) and.
 
 (* Program Instance and_impl_iff_morphism :  *)
@@ -49,7 +49,7 @@ Program Instance and_iff_morphism :
 
 (** Logical disjunction. *)
 
-Program Instance or_impl_iff_morphism : 
+Program Instance or_impl_morphism : 
   Morphism (impl ==> impl ==> impl) or.
 
 (* Program Instance or_impl_iff_morphism :  *)
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 5018fa01e..1b3896678 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -48,3 +48,11 @@ Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed
 Instance subrelation_pointwise :
   Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id.
 Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed.
+
+
+Lemma inverse_pointwise_relation A (R : relation A) : 
+  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
+Proof. intros. split; firstorder. Qed.
+
+
+
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 31398aa3b..c4e98c24a 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -21,13 +21,14 @@ Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Export Coq.Relations.Relation_Definitions.
 
+(** We allow to unfold the [relation] definition while doing morphism search. *)
+
+Typeclasses unfold relation.
+
 Notation inverse R := (flip (R:relation _) : relation _).
 
 Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
 
-Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
-  fun f g => forall x : A, R (f x) (g x).
-
 (** These are convertible. *)
 
 Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
@@ -394,7 +395,3 @@ Program Instance subrelation_partial_order :
   Proof.
     unfold relation_equivalence in *. firstorder.
   Qed.
-
-Lemma inverse_pointwise_relation A (R : relation A) : 
-  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
-Proof. reflexivity. Qed.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 227a93207..adeb38d49 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -41,13 +41,13 @@ Typeclasses unfold equiv.
 (** Shortcuts to make proof search easier. *)
 
 Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
-Proof. eauto with typeclass_instances. Qed.
+Proof. typeclasses eauto. Qed.
 
 Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
-Proof. eauto with typeclass_instances. Qed.
+Proof. typeclasses eauto. Qed.
 
 Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
-Proof. eauto with typeclass_instances. Qed.
+Proof. typeclasses eauto. Qed.
 
 Existing Instance setoid_refl.
 Existing Instance setoid_sym.
@@ -123,7 +123,7 @@ Ltac setoidify := repeat setoidify_tac.
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
 Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
-  trans_sym_morphism.
+  PER_morphism.
 
 (** Add this very useful instance in the database. *)
 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index e033343d1..20f4623f9 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -660,6 +660,8 @@ Add Relation key E.eq
  transitivity proved by E.eq_trans 
  as KeySetoid.
 
+Typeclasses unfold key.
+
 Implicit Arguments Equal [[elt]].
 
 Add Parametric Relation (elt : Type) : (t elt) Equal  
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 6afb8fcb7..4d24f54f4 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -309,6 +309,8 @@ Add Relation elt E.eq
  transitivity proved by E.eq_trans 
  as EltSetoid.
 
+Typeclasses unfold elt.
+
 Add Relation t Equal 
  reflexivity proved by eq_refl 
  symmetry proved by eq_sym
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 947dc818e..bb2c01437 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -102,6 +102,8 @@ exact sub_opp.
 exact add_opp.
 Qed.
 
+Typeclasses unfold NZadd NZmul NZsub NZeq.
+
 Add Ring BigZr : BigZring.
 
 (** Todo: tactic translating from [BigZ] to [Z] + omega *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index cbf6f701f..5376027dd 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -30,6 +30,7 @@ Module Make (N:NType) <: ZType.
   | Neg : N.t -> t_.
  
  Definition t := t_.
+ Typeclasses unfold t.
 
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 485480fa0..1e0b45cd2 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -76,6 +76,8 @@ exact mul_assoc.
 exact mul_add_distr_r.
 Qed.
 
+Typeclasses unfold NZadd NZsub NZmul.
+
 Add Ring BigNr : BigNring.
 
 (** Todo: tactic translating from [BigN] to [Z] + omega *)
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 0baba94c6..c360f53dc 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -139,7 +139,7 @@ let _ =
   pr "";
   pr " Definition %s := %s_." t t;
   pr "";
-
+  pr " Typeclasses unfold %s." t;
   pr " Definition w_0 := w0_op.(znz_0).";
   pr "";