- New auto hints for transparency/opacity control, not bound to

syntax yet. Doesn't change the auto/eauto behavior either.
- Typeclass resolution now considers everything transparent by 
default and does it consistently for "open" and closed terms.
- Correctly declare singleton classes definition as opaque for proof
search.
- Add a few initial declarations to make iff, id, compose... opaque
- Add definition of dependent signatures for dependent function types
and remove corresponding exception code in class_tactics. The 
instance requires higher-order unification and is not really usable yet.


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

14 files changed, 217 insertions, 87 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index bd335d3049..971dada68f 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]
-				      [Auto.Hint_db.empty false]
+				      [Auto.Hint_db.empty empty_transparent_state false]
 				  )
 			   )
 			)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index e368ff637e..09e61719ae 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1795,6 +1795,16 @@ let rec xlate_vernac =
 			    CT_id_ne_list(n1, names), dblist)
 	   else	     
              CT_hints(CT_ident "Unfold", CT_id_ne_list(n1, names), dblist)
+        | HintsTransparency (l,b) -> 
+	 let n1, names = match List.map loc_qualid_to_ct_ID l with
+	     n1 :: names -> n1, names
+	   | _  -> failwith "" in
+	 let ty = if b then "Transparent" else "Opaque" in
+	   if local then
+             CT_local_hints(CT_ident ty,
+			    CT_id_ne_list(n1, names), dblist)
+	   else	     
+             CT_hints(CT_ident ty, CT_id_ne_list(n1, names), dblist)
        	| HintsDestruct(id, n, loc, f, t) ->
 	    let dl = match loc with
 		ConclLocation() -> CT_conclusion_location
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 99d8e3c4a1..bfcaf99164 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -199,6 +199,9 @@ let pr_hints local db h pr_c pr_pat =
         str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l
     | HintsUnfold l ->
         str "Unfold " ++ prlist_with_sep sep pr_reference l
+    | HintsTransparency (l, b) ->
+        str (if b then "Transparent " else "Opaque ") ++ prlist_with_sep sep 
+	  pr_reference l
     | HintsConstructors c ->
         str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c
     | HintsExtern (n,c,tac) ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 7e10264ef4..3624fe792d 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -784,6 +784,11 @@ let pr_instance env i =
   (* lighter *)
   print_ref false (ConstRef (instance_impl i))
     
+let print_all_instances () =
+  let env = Global.env () in
+  let inst = all_instances () in 
+    prlist_with_sep fnl (pr_instance env) inst
+
 let print_instances r =
   let env = Global.env () in
   let inst = instances r in 
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index db1d8bb109..88b0a80ecc 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -61,7 +61,7 @@ val print_canonical_projections : unit -> std_ppcmds
 (* Pretty-printing functions for type classes and instances *)
 val print_typeclasses : unit -> std_ppcmds
 val print_instances : global_reference -> std_ppcmds
-
+val print_all_instances : unit -> std_ppcmds
 
 val inspect : int -> std_ppcmds
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 53e493d143..a1550d8cbc 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -118,9 +118,9 @@ module Hint_db = struct
     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 empty st use_dn = { hintdb_state = st;
+			  use_dn = use_dn;
+			  hintdb_map = Constr_map.empty }
     
   let find key db =
     try Constr_map.find key db.hintdb_map
@@ -328,15 +328,29 @@ let add_hint dbname hintlist =
     let db' = Hint_db.add_list hintlist db in
     searchtable_add (dbname,db')
   with Not_found -> 
-    let db = Hint_db.add_list hintlist (Hint_db.empty false) in
+    let db = Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false) in
     searchtable_add (dbname,db)
 
-type hint_action = CreateDB of bool | UpdateDB of (global_reference * pri_auto_tactic) list
+let add_transparency dbname grs b =
+  let db = searchtable_map dbname in
+  let st = Hint_db.transparent_state db in
+  let st' = 
+    List.fold_left (fun (ids, csts) gr -> 
+      match gr with
+      | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts)
+      | EvalVarRef v -> (if b then Idpred.add else Idpred.remove) v ids, csts)
+      st grs
+  in searchtable_add (dbname, Hint_db.set_transparent_state db st')
+    
+type hint_action = | CreateDB of bool * transparent_state
+		   | AddTransparency of evaluable_global_reference list * bool
+		   | AddTactic 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
+  | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
+  | AddTransparency (grs, b) -> add_transparency name grs b
+  | AddTactic hints -> add_hint name hints
 
 let forward_subst_tactic = 
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
@@ -388,13 +402,16 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
   in
     match hintlist with
     | CreateDB _ -> obj
-    | UpdateDB hintlist ->
+    | AddTransparency (grs, b) -> 
+	let grs' = list_smartmap (subst_evaluable_reference subst) grs in
+	  if grs==grs' then obj else (local, name, AddTransparency (grs', b))
+    | AddTactic hintlist ->
 	let hintlist' = list_smartmap subst_hint hintlist in
 	  if hintlist' == hintlist then obj else
-	    (local,name,UpdateDB hintlist')
+	    (local,name,AddTactic hintlist')
 	      
 let classify_autohint (_,((local,name,hintlist) as obj)) =
-  if local or hintlist = (UpdateDB []) then Dispose else Substitute obj
+  if local or hintlist = (AddTactic []) then Dispose else Substitute obj
 
 let export_autohint ((local,name,hintlist) as obj) =
   if local then None else Some obj
@@ -408,8 +425,8 @@ let (inAutoHint,outAutoHint) =
                     export_function = export_autohint }
 
 
-let create_hint_db l n b = 
-  Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB b))
+let create_hint_db l n st b = 
+  Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
       
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
@@ -419,7 +436,7 @@ let add_resolves env sigma clist local dbnames =
     (fun dbname ->
        Lib.add_anonymous_leaf
 	 (inAutoHint
-	    (local,dbname, UpdateDB
+	    (local,dbname, AddTactic
      	      (List.flatten (List.map (fun (x, y) ->
 		make_resolves env sigma (true,Flags.is_verbose()) x y) clist)))))
     dbnames
@@ -428,7 +445,13 @@ let add_resolves env sigma clist local dbnames =
 let add_unfolds l local dbnames =
   List.iter 
     (fun dbname -> Lib.add_anonymous_leaf 
-       (inAutoHint (local,dbname, UpdateDB (List.map make_unfold l))))
+       (inAutoHint (local,dbname, AddTactic (List.map make_unfold l))))
+    dbnames
+
+let add_transparency l b local dbnames =
+  List.iter 
+    (fun dbname -> Lib.add_anonymous_leaf 
+       (inAutoHint (local,dbname, AddTransparency (l, b))))
     dbnames
 
 let add_extern pri (patmetas,pat) tacast local dbname =
@@ -441,7 +464,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, UpdateDB [make_extern pri pat tacast]))
+	  (inAutoHint(local,dbname, AddTactic [make_extern pri pat tacast]))
 
 let add_externs pri pat tacast local dbnames = 
   List.iter (add_extern pri pat tacast local) dbnames
@@ -450,7 +473,7 @@ let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(local,dbname, UpdateDB (List.map (make_trivial env sigma) l))))
+	 inAutoHint(local,dbname, AddTactic (List.map (make_trivial env sigma) l))))
     dbnames
 
 let forward_intern_tac = 
@@ -481,6 +504,20 @@ let add_hints local dbnames0 h =
 	  Dumpglob.add_glob (loc_of_reference r) gr;
 	 (gr,r') in
       add_unfolds (List.map f lhints) local dbnames
+ | HintsTransparency (lhints, b) ->
+      let f r =
+	let gr = Syntax_def.global_with_alias r in
+        let r' = match gr with
+         | ConstRef c -> EvalConstRef c
+         | VarRef c -> EvalVarRef c
+         | _ -> 
+           errorlabstrm "evalref_of_ref"
+            (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
+             str "to an evaluable reference.")
+        in
+	  Dumpglob.add_glob (loc_of_reference r) gr;
+	  r' in
+      add_transparency (List.map f lhints) b local dbnames
   | HintsConstructors lqid ->
       let add_one qid =
         let env = Global.env() and sigma = Evd.empty in
@@ -651,7 +688,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
-    Hint_db.add_list hintlist' (Hint_db.add_list hintlist (Hint_db.empty false))
+    Hint_db.add_list hintlist' (Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state 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
diff --git a/tactics/auto.mli b/tactics/auto.mli
index c5df28d427..27ecca9830 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -47,7 +47,7 @@ type search_entry = stored_data list * stored_data list * stored_data Btermdn.t
 module Hint_db :
   sig
     type t
-    val empty : bool -> t
+    val empty : transparent_state -> 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
@@ -68,7 +68,7 @@ val searchtable_map : hint_db_name -> hint_db
 
 val searchtable_add : (hint_db_name * hint_db) -> unit
 
-val create_hint_db : bool -> hint_db_name -> bool -> unit
+val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
 
 val current_db_names : unit -> hint_db_name list
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 68f9aa9221..148c961c76 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -43,7 +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 false)
+let _ = Auto.auto_init := (fun () -> 
+  Auto.create_hint_db false typeclasses_db full_transparent_state false)
 
 let check_imported_library d =
   let d' = List.map id_of_string d in
@@ -89,20 +90,22 @@ let auto_unif_flags = {
   modulo_delta = var_full_transparent_state;
 }
 
-let unify_e_resolve st (c,clenv) gls = 
+let unify_e_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
-  let clenv' = clenv_unique_resolver false
-    ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls 
+  let clenv' = clenv_unique_resolver false ~flags clenv' gls 
   in
     Clenvtac.clenv_refine true clenv' gls
       
-let unify_resolve st (c,clenv) gls = 
+let unify_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
-  let clenv' = clenv_unique_resolver false
-    ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls 
+  let clenv' = clenv_unique_resolver false ~flags clenv' gls 
   in
     Clenvtac.clenv_refine false clenv' gls
 
+let flags_of_state st =
+  {auto_unif_flags with 
+    modulo_conv_on_closed_terms = Some st; modulo_delta = st}
+
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl = 
     Eauto.registered_e_assumption ::
@@ -122,25 +125,25 @@ and e_my_find_search db_list local_db hdc concl =
     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))
+	  let flags = flags_of_state (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 db -> 
-	  let st = Hint_db.transparent_state db in
-	    List.map (fun x -> (st, x)) (Hint_db.map_auto (hdc,concl) db))
+	  let flags = flags_of_state (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}) -> 
+    fun (flags, {pri=b; pat = p; code=t}) -> 
       let tac =
 	match t with
-	  | Res_pf (term,cl) -> unify_resolve st (term,cl)
-	  | ERes_pf (term,cl) -> unify_e_resolve st (term,cl)
+	  | Res_pf (term,cl) -> unify_resolve flags (term,cl)
+	  | ERes_pf (term,cl) -> unify_e_resolve flags (term,cl)
 	  | Give_exact (c) -> e_give_exact c
 	  | Res_pf_THEN_trivial_fail (term,cl) ->
-              tclTHEN (unify_e_resolve st (term,cl)) 
+              tclTHEN (unify_e_resolve flags (term,cl)) 
 		(e_trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	  | Extern tacast -> conclPattern concl 
@@ -415,16 +418,23 @@ let valid goals p res_sigma l =
 	  else sigma)
       !res_sigma goals l
   in raise (Found evm)
+
+let is_dependent ev evm = 
+  Evd.fold (fun ev' evi dep -> 
+    if ev = ev' then dep
+    else dep || occur_evar ev evi.evar_concl)
+    evm false
     
 let resolve_all_evars_once debug (mode, depth) env p evd =
   let evm = Evd.evars_of evd in
   let goals, evm' = 
     Evd.fold
-      (fun ev evi (gls, evm) ->
+      (fun ev evi (gls, evm') ->
 	if evi.evar_body = Evar_empty 
 	  && Typeclasses.is_resolvable evi
-	  && p ev evi then ((ev,evi) :: gls, Evd.add evm ev (Typeclasses.mark_unresolvable evi)) else 
-	  (gls, Evd.add evm ev evi))
+(* 	  && not (is_dependent ev evm) *)
+	  && p ev evi then ((ev,evi) :: gls, Evd.add evm' ev (Typeclasses.mark_unresolvable evi)) else 
+	  (gls, Evd.add evm' ev evi))
       evm ([], Evd.empty)
   in
   let goals = List.rev goals in
@@ -501,7 +511,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
 		  (fun ev evi (b,acc) -> 
 		    (* focus on one instance if only one was searched for *)
 		    if class_of_constr evi.evar_concl <> None then
-		      if not b then
+		      if not b (* || do_split *) then
 			true, Some ev 
 		      else b, None
 		    else b, acc) evm (false, None)
@@ -532,19 +542,11 @@ VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
     add_hints false [typeclasses_db] (Vernacexpr.HintsUnfold cl)
   ]
 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')
- ]
+| [ "Typeclasses" "Opaque" reference_list(cl) ] -> [
+    add_hints false [typeclasses_db] (Vernacexpr.HintsTransparency (cl, false))
+  ]
 END
 
 (** Typeclass-based rewriting. *)
@@ -580,8 +582,10 @@ let coq_inverse = lazy (gen_constant (* ["Classes"; "RelationClasses"] "inverse"
 			   ["Program"; "Basics"] "flip")
 
 let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |])
+(* let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; new_Type (); rel |]) *)
 
 let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement")
+let forall_relation = lazy (gen_constant ["Classes"; "Morphisms"] "forall_relation")
 let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation")
 
 let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep")
@@ -592,6 +596,8 @@ let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultR
 
 let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation")
 let mk_relation a = mkApp (Lazy.force coq_relation, [| a |])
+(* let mk_relation a = mkProd (Anonymous, a, mkProd (Anonymous, a, new_Type ())) *)
+
 let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
 
 let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive")
@@ -638,8 +644,6 @@ let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
 
-exception DependentMorphism
-
 let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.t option) (f : 'a -> constr) =
   let new_evar isevars env t =
     Evarutil.e_new_evar isevars env
@@ -656,12 +660,17 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
     let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) ty in
       match kind_of_term t, l with
       | Prod (na, ty, b), obj :: cstrs -> 
-	  if dependent (mkRel 1) ty then raise DependentMorphism;
 	  let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in
 	  let ty = Reductionops.nf_betaiota ty in
-	  let relty = mk_relty ty obj in
-	  let arg' = mkApp (Lazy.force respectful, [| ty ; b ; relty ; arg |]) in
-	    mkProd(na, ty, b), arg', (ty, relty) :: evars
+	    if dependent (mkRel 1) ty then
+	      let pred = mkLambda (na, ty, b) in
+	      let liftarg = mkLambda (na, ty, arg) in
+	      let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
+		mkProd(na, ty, b), arg', evars
+	    else
+	      let relty = mk_relty ty obj in
+	      let arg' = mkApp (Lazy.force respectful, [| ty ; b ; relty ; arg |]) in
+		mkProd(na, ty, b), arg', (ty, relty) :: evars
       | _, obj :: _ -> anomaly "build_signature: not enough products"
       | _, [] -> 
 	  (match finalcstr with
@@ -1041,9 +1050,11 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
       | None -> pf_concl gl, None
   in
   let cstr = 
-    match is_hyp with
-	None -> (mkProp, inverse mkProp (Lazy.force impl))
-      | Some _ -> (mkProp, Lazy.force impl)
+    let sort = mkProp in
+    let impl = Lazy.force impl in
+      match is_hyp with
+      | None -> (sort, inverse sort impl)
+      | Some _ -> (sort, impl)
   in
   let evars = ref (Evd.create_evar_defs Evd.empty) in
   let env = pf_env gl in
@@ -1104,8 +1115,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
 	    (* tclFAIL 1 (str"setoid rewrite failed") gl *)
 	  
 let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl =
-  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
+  cl_rewrite_clause_aux ~flags hypinfo goal_meta occs clause gl
 
 let cl_rewrite_clause (evm,c) left2right occs clause gl =
   init_setoid ();
@@ -1473,8 +1483,7 @@ let default_morphism sign m =
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let t = Typing.type_of env Evd.empty m in
   let _, sign, evars =
-    try build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
-    with DependentMorphism -> error "Cannot infer the signature of dependent morphisms"
+    build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
   in
   let morph =
     mkApp (Lazy.force morphism_type, [| t; sign; m |])
@@ -1497,9 +1506,7 @@ let add_setoid binders a aeq t n =
 let add_morphism_infer m n =
   init_setoid ();
   let instance_id = add_suffix n "_Morphism" in
-  let instance = try build_morphism_signature m 
-    with DependentMorphism -> error "Cannot infer the signature of dependent morphisms"
-  in
+  let instance = build_morphism_signature m in
     if Lib.is_modtype () then 
       let cst = Declare.declare_internal_constant instance_id
 	(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
@@ -1637,35 +1644,38 @@ let is_loaded d =
 let try_loaded f gl =
   if is_loaded ["Coq";"Classes";"RelationClasses"] then f gl
   else tclFAIL 0 (str"You need to require Coq.Classes.RelationClasses first") gl
+
+let not_declared env ty car rel =
+  tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ 
+		str ty ++ str" relation on carrier " ++ Printer.pr_constr_env env car)
     
 let setoid_reflexivity gl =
   let env = pf_env gl in
   let rel, args = relation_of_constr (pf_concl gl) in
+  let car = pf_type_of gl args.(0) in
     try
-      apply (reflexive_proof env (pf_type_of gl args.(0)) rel) gl
-    with Not_found -> 
-      tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared reflexive relation")
-	gl
+      apply (reflexive_proof env car rel) gl
+    with Not_found -> not_declared env "reflexive" car rel gl
 	  
 let setoid_symmetry gl =
   let env = pf_env gl in
   let rel, args = relation_of_constr (pf_concl gl) in
+  let car = pf_type_of gl args.(0) in
     try
-      apply (symmetric_proof env (pf_type_of gl args.(0)) rel) gl
+      apply (symmetric_proof env car rel) gl
     with Not_found -> 
-      tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared symmetric relation")
-	gl
+      not_declared env "symmetric" car rel gl
 	
 let setoid_transitivity c gl =
   let env = pf_env gl in
   let rel, args = relation_of_constr (pf_concl gl) in
+  let car = pf_type_of gl c in
     try
       apply_with_bindings
-	((transitive_proof env (pf_type_of gl args.(0)) rel),
+	((transitive_proof env car rel),
 	Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]) gl
     with Not_found -> 
-      tclFAIL 0
-	(str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared transitive relation") gl
+      not_declared env "transitive" car rel gl
 
 let setoid_symmetry_in id gl =
   let ctype = pf_type_of gl (mkVar id) in
@@ -1755,3 +1765,47 @@ TACTIC EXTEND head_of_constr
       letin_tac None (Name h) c allHyps
   ]
 END
+
+
+let coq_List_nth =  lazy (gen_constant ["Lists"; "List"] "nth")
+let coq_List_cons =  lazy (gen_constant ["Lists"; "List"] "cons")
+let coq_List_nil =  lazy (gen_constant ["Lists"; "List"] "nil")
+
+let freevars c =
+  let rec frec acc c = match kind_of_term c with
+    | Var id       -> Idset.add id acc
+    | _ -> fold_constr frec acc c
+  in 
+  frec Idset.empty c
+
+let coq_zero =  lazy (gen_constant ["Init"; "Datatypes"] "O")
+let coq_succ =  lazy (gen_constant ["Init"; "Datatypes"] "S")
+
+let rec coq_nat_of_int = function
+  | 0 -> Lazy.force coq_zero
+  | n -> mkApp (Lazy.force coq_succ, [| coq_nat_of_int (pred n) |])
+
+let varify_constr ty def varh c =
+  let vars = Idset.elements (freevars c) in
+  let mkaccess i = 
+    mkApp (Lazy.force coq_List_nth,
+	  [| ty; coq_nat_of_int i; varh; def |])
+  in
+  let l = List.fold_right (fun id acc -> 
+    mkApp (Lazy.force coq_List_cons, [| ty ; mkVar id; acc |]))
+    vars (mkApp (Lazy.force coq_List_nil, [| ty |]))
+  in
+  let subst = 
+    list_map_i (fun i id -> (id, mkaccess i)) 0 vars
+  in
+    l, replace_vars subst c
+
+TACTIC EXTEND varify
+  [ "varify" ident(varh) ident(h') constr(ty) constr(def) constr(c) ] -> [
+    let vars, c' = varify_constr ty def (mkVar varh) c in
+      tclTHEN (letin_tac None (Name varh) vars allHyps)
+	(letin_tac None (Name h') c' allHyps)
+  ]
+END
+
+
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 22d9ff56f7..03b0e9ad5d 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -138,6 +137,6 @@ Program Instance pointwise_equivalence [ eqb : Equivalence B eqB ] :
 
   Next Obligation.
   Proof.
-    transitivity (y x0) ; auto.
+    transitivity (y a) ; auto.
   Qed.
 
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index dd082246cc..5ac9310330 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -20,6 +20,12 @@
 Tactic Notation "clapply" ident(c) :=
   eapply @c ; typeclasses eauto.
 
+(** Hints for the proof search: these combinators should be considered rigid. *)
+
+Require Import Program.Basics.
+
+Typeclasses Opaque id const flip compose arrow impl iff.
+
 (** The unconvertible typeclass, to test that two objects of the same type are 
    actually different. *)
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8acbe916b1..270b9d8aca 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -75,10 +75,17 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
 
 Open Local Scope signature_scope.
 
-(** Pointwise lifting is just respect with leibniz equality on the left. *)
+(** Dependent pointwise lifting of a relation on the range. *) 
+
+Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) :=
+  λ f g, Π a : A, sig a (f a) (g a).
+
+Arguments Scope forall_relation [type_scope type_scope signature_scope].
+
+(** Non-dependent pointwise lifting *)
 
 Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
-  fun f g => forall x : A, R (f x) (g x).
+  Eval compute in forall_relation (B:=λ _, B) (λ _, R).
 
 Lemma pointwise_pointwise A B (R : relation B) : 
   relation_equivalence (pointwise_relation R) (@eq A ==> R).
@@ -91,12 +98,14 @@ Hint Unfold Reflexive : core.
 Hint Unfold Symmetric : core.
 Hint Unfold Transitive : core.
 
+Typeclasses Opaque respectful pointwise_relation forall_relation.
+
 Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : 
   PER (A -> B) (R ==> R').
 
   Next Obligation.
   Proof with auto.
-    assert(R x0 x0). 
+    assert(R x0 x0).
     transitivity y0... symmetry...
     transitivity (y x0)...
   Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index bdd7b4b1d1..dcf3139b2d 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -23,12 +23,13 @@ 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.
 
+(** Opaque for proof-search. *)
+Typeclasses Opaque complement.
+
 (** These are convertible. *)
 
 Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9f3b3343cb..288574882b 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -32,16 +32,20 @@ open Topconstr
 open Decl_kinds
 open Entries
 
-let hint_db = "typeclass_instances"
+let typeclasses_db = "typeclass_instances"
 
 let qualid_of_con c = 
   Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
 
+let set_rigid c = 
+  Auto.add_hints false [typeclasses_db] 
+    (Vernacexpr.HintsTransparency ([qualid_of_con c], false))
+
 let _ =
   Typeclasses.register_add_instance_hint 
     (fun inst pri ->
       Flags.silently (fun () ->      
-	Auto.add_hints false [hint_db] 
+	Auto.add_hints false [typeclasses_db] 
 	  (Vernacexpr.HintsResolve 
 	      [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ())
 
@@ -228,6 +232,7 @@ let new_class id par ar sup props =
 	    let cref = ConstRef cst in
 	      Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps;
 	      Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls);
+	      set_rigid cst;
 	      cref, [proj_name, proj_cst]
 	| _ ->
 	    let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e1b3164810..5bd8dc36eb 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -115,6 +115,7 @@ type hints =
   | HintsResolve of (int option * constr_expr) list
   | HintsImmediate of constr_expr list
   | HintsUnfold of reference list
+  | HintsTransparency of reference list * bool
   | HintsConstructors of reference list
   | HintsExtern of int * constr_expr * raw_tactic_expr
   | HintsDestruct of identifier *