- Parameterize unification by two sets of transparent_state, one for open

term unification (for constant and variable delta unfolding) and one to
parameterize closed-term conversion. Most of the time conversion uses
full delta and unification does no delta. This fine-grain is used in
rewrite/setoid_rewrite, where only closed-term delta on global constants
is allowed.
- Interpret Hint Unfold as a directive for delta conversion in
auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints).
- Remove ad-hoc support for this in typeclasses. Now setoid_rewrite
works correctly w.r.t. the old version regarding local definitions.
- Fix closed bugs which needed updating due to syntax modifications.


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

7 files changed, 117 insertions, 222 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 00d7b8cb4..2709502c6 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -137,14 +137,16 @@ end
 
 module Hintdbmap = Gmap
 
-type frozen_hint_db_table = (string,Hint_db.t) Hintdbmap.t 
+type hint_db = Names.transparent_state * Hint_db.t
 
-type hint_db_table = (string,Hint_db.t) Hintdbmap.t ref
+type frozen_hint_db_table = (string,hint_db) Hintdbmap.t 
+
+type hint_db_table = (string,hint_db) Hintdbmap.t ref
 
 type hint_db_name = string
 
 let searchtable = (ref Hintdbmap.empty : hint_db_table)
-
+  
 let searchtable_map name = 
   Hintdbmap.find name !searchtable
 let searchtable_add (name,db) = 
@@ -277,18 +279,32 @@ 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' = Hint_db.add_list hintlist db in
+    let db' = add_hint_list hintlist db in
     searchtable_add (dbname,db')
   with Not_found -> 
-    let db = Hint_db.add_list hintlist Hint_db.empty in
+    let db = add_hint_list hintlist (empty_transparent_state, Hint_db.empty) in
     searchtable_add (dbname,db)
 
-let cache_autohint (_,(local,name,hintlist)) = add_hint name hintlist
+let cache_autohint (_,(local,name,hints)) = add_hint name hints
 
 let forward_subst_tactic = 
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
@@ -476,7 +492,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 
@@ -502,11 +518,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 
@@ -537,14 +553,14 @@ let print_hint_db db =
 
 let print_hint_db_by_name dbname =
   try 
-    let db = searchtable_map dbname in print_hint_db db
+    let db = snd (searchtable_map dbname) in print_hint_db db
   with Not_found -> 
     error (dbname^" : No such Hint database")
   
 (* displays all the hints of all databases *)
 let print_searchtable () =
   Hintdbmap.iter
-    (fun name db ->
+    (fun name (_, db) ->
        msg (str "In the database " ++ str name ++ fnl ());
        print_hint_db db)
     !searchtable
@@ -565,17 +581,16 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
 open Unification
 
 let auto_unif_flags = {
-  modulo_conv_on_closed_terms = true; 
+  modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = false;
-  modulo_delta = Cpred.empty;
-  modulo_zeta = true;
+  modulo_delta = empty_transparent_state;
 }
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let unify_resolve (c,clenv) gls = 
+let unify_resolve st (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gls in  
+  let _ = clenv_unique_resolver false ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls in  
   h_simplest_apply c gls
 
 (* builds a hint database from a constr signature *)
@@ -585,7 +600,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)
+    (empty_transparent_state, Hint_db.add_list hintlist' (Hint_db.add_list hintlist Hint_db.empty))
 
 (* 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
@@ -623,7 +638,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 (Hint_db.add_list hintl local_db) g')
+	 in trivial_fail_db db_list (add_hint_list hintl local_db) g')
   in
   tclFIRST 
     (assumption::intro_tac::
@@ -633,21 +648,24 @@ let rec trivial_fail_db db_list local_db gl =
 and my_find_search db_list local_db hdc concl =
   let tacl = 
     if occur_existential concl then 
-      list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list)
+      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 db -> Hint_db.map_auto (hdc,concl) db)
+      list_map_append (fun (st, db) -> 
+	List.map (fun x -> (st,x)) (Hint_db.map_auto (hdc,concl) db))
       	(local_db::db_list)
   in
-  List.map 
-    (fun {pri=b; pat=p; code=t} -> 
-       (b,
+    List.map 
+      (fun (st, {pri=b; pat=p; code=t}) -> 
+	(b,
 	match t with
-	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
+	  | Res_pf (term,cl)  -> unify_resolve st (term,cl)
 	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
 	  | Give_exact c  -> exact_check c
 	  | Res_pf_THEN_trivial_fail (term,cl) -> 
 	      tclTHEN 
-		(unify_resolve (term,cl)) 
+		(unify_resolve st (term,cl)) 
 		(trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> unfold_in_concl [[],c]
 	  | Extern tacast -> 
@@ -749,7 +767,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 		(mkVar hid, htyp)]
 	   with Failure _ -> [] 
 	 in
-         search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d] g') 
+         search_gen decomp n db_list (add_hint_list hintl local_db) [d] g') 
   in
   let rec_tacs = 
     List.map 
@@ -881,7 +899,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 (Hint_db.add_list hintl local_db)
+	   super_search n db_list (add_hint_list hintl local_db)
 	     argl g))
      ::
      ((List.map 
@@ -899,7 +917,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 = Hint_db.add_list db0 (make_local_hint_db false [] g) in
+  let db = add_hint_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 4fe9f03a9..bb22b6c81 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -58,10 +58,14 @@ module Hint_db :
 
 type hint_db_name = string
 
-val searchtable_map : hint_db_name -> Hint_db.t
+type hint_db = transparent_state * Hint_db.t
+
+val searchtable_map : hint_db_name -> hint_db
 
 val current_db_names : unit -> hint_db_name list
 
+val add_hint_list : (global_reference * pri_auto_tactic) list -> hint_db -> hint_db
+
 val add_hints : locality_flag -> hint_db_name list -> hints -> unit
 
 val print_searchtable : unit -> unit
@@ -128,14 +132,14 @@ val set_extern_subst_tactic :
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)
 
-val make_local_hint_db : bool -> constr list -> goal sigma -> Hint_db.t
+val make_local_hint_db : bool -> constr list -> goal sigma -> hint_db
 
 val priority : (int * 'a) list -> 'a list
 
 val default_search_depth : int ref
 
 (* Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : (constr * clausenv) -> tactic
+val unify_resolve : transparent_state -> (constr * clausenv) -> tactic
 
 (* [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a1d978b1f..b46d0e05e 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -40,18 +40,18 @@ open Command
 open Libnames
 open Evd
 
-let check_required_library d =
+let check_imported_library d =
   let d' = List.map id_of_string d in
   let dir = make_dirpath (List.rev d') in
-  if (* not (Library.library_is_opened dir) ||  *)not (Library.library_is_loaded dir) then
-    error ("Library "^(list_last d)^" has to be required first")
-
+  if not (Library.library_is_loaded dir) then
+    error ("Library "^(list_last d)^" has to be imported first")
+      
 let classes_dirpath =
   make_dirpath (List.map id_of_string ["Classes";"Coq"])
   
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
-  else check_required_library ["Coq";"Setoids";"Setoid"]
+  else check_imported_library ["Coq";"Setoids";"Setoid"]
 
 (** Typeclasses instance search tactic / eauto *)
 
@@ -67,21 +67,24 @@ let assumption id = e_give_exact (mkVar id)
 
 open Unification
 
-let auto_unif_flags = ref {
-  modulo_conv_on_closed_terms = true; 
+let auto_unif_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
-  modulo_delta = Cpred.empty;
-  modulo_zeta = true;
+  modulo_delta = var_full_transparent_state;
 }
 
-let unify_e_resolve (c,clenv) gls = 
+let unify_e_resolve st (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
-  let clenv' = clenv_unique_resolver false ~flags:(!auto_unif_flags) clenv' gls in
+  let clenv' = clenv_unique_resolver false
+    ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls 
+  in
     Clenvtac.clenv_refine true clenv' gls
-
-let unify_resolve (c,clenv) gls = 
+      
+let unify_resolve st (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
-  let clenv' = clenv_unique_resolver false ~flags:(!auto_unif_flags) clenv' gls in  
+  let clenv' = clenv_unique_resolver false
+    ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls 
+  in
     Clenvtac.clenv_refine false clenv' gls
 
 let rec e_trivial_fail_db db_list local_db goal =
@@ -92,7 +95,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
-	     (Hint_db.add_list hintl local_db) g'))) ::
+	     (add_hint_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 
@@ -101,19 +104,23 @@ 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
-      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
+      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 (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
+      list_map_append
+	(fun (st, db) -> List.map (fun x -> (st, x)) (Hint_db.map_auto (hdc,concl) db))
+	(local_db::db_list)
   in 
   let tac_of_hint = 
-    fun {pri=b; pat = p; code=t} -> 
+    fun (st, {pri=b; pat = p; code=t}) -> 
       let tac =
 	match t with
-	  | Res_pf (term,cl) -> unify_resolve (term,cl)
-	  | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
+	  | Res_pf (term,cl) -> unify_resolve st (term,cl)
+	  | ERes_pf (term,cl) -> unify_e_resolve st (term,cl)
 	  | Give_exact (c) -> e_give_exact c
 	  | Res_pf_THEN_trivial_fail (term,cl) ->
-              tclTHEN (unify_e_resolve (term,cl)) 
+              tclTHEN (unify_e_resolve st (term,cl)) 
 		(e_trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> unfold_in_concl [[],c]
 	  | Extern tacast -> conclPattern concl 
@@ -144,9 +151,8 @@ type search_state = {
   tacres : goal list sigma * validation;
   pri : int;
   last_tactic : std_ppcmds;
-(*   filter : constr -> constr -> bool; *)
-  dblist : Auto.Hint_db.t list;
-  localdb :  Auto.Hint_db.t list }
+  dblist : Auto.hint_db list;
+  localdb :  Auto.hint_db list }
     
 let filter_hyp t = 
   match kind_of_term t with
@@ -215,7 +221,6 @@ module SearchProblem = struct
       let nbgl = List.length (sig_it lg) in
       assert (nbgl > 0);
       let g = find_first_goal lg in
-(*       let filt = s.filter (pf_concl g) in *)
       let assumption_tacs = 
 	let l = 
 	  filter_tactics s.tacres
@@ -314,7 +319,6 @@ let make_initial_state n gls dblist localdbs =
   { depth = n;
     tacres = gls;
     pri = 0;
-(*     filter = filter; *)
     last_tactic = (mt ());
     dblist = dblist;
     localdb = localdbs }
@@ -395,9 +399,6 @@ let has_undefined p evd =
     (Evd.evars_of evd) false
     
 let resolve_all_evars debug m env p oevd =
-(*   let evd = resolve_all_evars_once ~tac debug m env p evd in *)
-(*     if has_undefined p evd then raise Not_found *)
-(*     else evd *)
   try
     let rec aux n evd =
       if has_undefined p evd then
@@ -409,77 +410,12 @@ let resolve_all_evars debug m env p oevd =
     in aux 3 oevd
   with Not_found -> None
     
-(** Handling of the state of unfolded constants. *)
-
-open Libobject
-
-let freeze () = !auto_unif_flags.modulo_delta
-
-let unfreeze delta = 
-  auto_unif_flags := { !auto_unif_flags with modulo_delta = delta }
-    
-let init () =
-  auto_unif_flags := {
-    modulo_conv_on_closed_terms = true; 
-    use_metas_eagerly = true;
-    modulo_delta = Cpred.empty;
-    modulo_zeta = true;
-  }
-    
-let _ = 
-  Summary.declare_summary "typeclasses_unfold"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = false;
-      Summary.survive_section = true }
-    
-let cache_autounfold (_,unfoldlist) = 
-  auto_unif_flags := { !auto_unif_flags with
-    modulo_delta = Cpred.union !auto_unif_flags.modulo_delta unfoldlist }
-  
-let subst_autounfold (_,subst,(unfoldlist as obj)) = 
-  let b, l' = Cpred.elements unfoldlist in
-  let l'' = list_smartmap (fun x -> fst (Mod_subst.subst_con subst x)) l' in
-    if l'' == l' then obj 
-    else
-      let set = List.fold_right Cpred.add l'' Cpred.empty in
-	if not b then set
-	else Cpred.complement set
-	  
-let classify_autounfold (_,obj) = Substitute obj
-      
-let export_autounfold obj =
-  Some obj
-
-let (inAutoUnfold,outAutoUnfold) =
-  declare_object 
-    {(default_object "AUTOUNFOLD") with
-      cache_function = cache_autounfold;
-      load_function = (fun _ -> cache_autounfold);
-      subst_function = subst_autounfold;
-      classify_function = classify_autounfold;
-      export_function = export_autounfold }
-
-let cpred_of_list l =
-  List.fold_right Cpred.add l Cpred.empty
-
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
-| [ "Typeclasses" "unfold" constr_list(cl) ] -> [
-    let csts = 
-      List.map
-	(fun c -> 
-	  let c = Constrintern.interp_constr Evd.empty (Global.env ()) c in
-	    match kind_of_term c with
-	      | Const c -> c
-	      | _ -> error "Not a constant reference")
-	cl
-    in
-      Lib.add_anonymous_leaf (inAutoUnfold (cpred_of_list csts))
+| [ "Typeclasses" "unfold" reference_list(cl) ] -> [
+    add_hints true ["typeclass_instances"] (Vernacexpr.HintsUnfold cl)
   ]
 END
 
-
 (** Typeclass-based rewriting. *)
 
 let respect_proj = lazy (mkConst (List.hd (Lazy.force morphism_class).cl_projs))
@@ -537,10 +473,7 @@ let arrow_morphism a b =
     Lazy.force impl
   else
     mkApp(Lazy.force arrow, [|a;b|])
-(*     mkLambda (Name (id_of_string "A"), a,  *)
-(* 	     mkLambda (Name (id_of_string "B"), b,  *)
-(* 		      mkProd (Anonymous, mkRel 2, mkRel 2))) *)
-    
+
 let setoid_refl pars x = 
   applistc (Lazy.force setoid_refl_proj) (pars @ [x])
       
@@ -666,10 +599,9 @@ type hypinfo = {
   abs : (constr * types) option;
 }
 
-let convertible env evd x y =
+let evd_convertible env evd x y =
   try ignore(Evarconv.the_conv_x env x y evd); true 
   with _ -> false
-    (* ignore(Reduction.conv env x y) *)
   
 let decompose_setoid_eqhyp env sigma c left2right =
   let ctype = Typing.type_of env sigma c in
@@ -684,7 +616,7 @@ let decompose_setoid_eqhyp env sigma c left2right =
   let ty1, ty2 = 
     Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
   in
-    if not (convertible env eqclause.evd ty1 ty2) then
+    if not (evd_convertible env eqclause.evd ty1 ty2) then
       error "The term does not end with an applied homogeneous relation"
     else
       { cl=eqclause; prf=(Clenv.clenv_value eqclause);
@@ -692,38 +624,22 @@ let decompose_setoid_eqhyp env sigma c left2right =
 	l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
 
 let rewrite_unif_flags = {
-  Unification.modulo_conv_on_closed_terms = false;
+  Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly = true;
-  Unification.modulo_delta = Cpred.empty;
-  Unification.modulo_zeta = false;
+  Unification.modulo_delta = empty_transparent_state;
 }
 
+let conv_transparent_state = (Idpred.empty, Cpred.full)
+
 let rewrite2_unif_flags = {
-  Unification.modulo_conv_on_closed_terms = true;
+  Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
   Unification.use_metas_eagerly = true;
-  Unification.modulo_delta = Cpred.empty;
-  Unification.modulo_zeta = false;
+  Unification.modulo_delta = empty_transparent_state;
 }
 
-(* let unification_rewrite c1 c2 cl but gl =  *)
-(*   let (env',c1) = *)
-(*     try *)
-(*       (\* ~flags:(false,true) to allow to mark occurrences that must not be *)
-(*          rewritten simply by replacing them with let-defined definitions *)
-(*          in the context *\) *)
-(*       w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd *)
-(*     with *)
-(* 	Pretype_errors.PretypeError _ -> *)
-(* 	  (\* ~flags:(true,true) to make Ring work (since it really *)
-(*              exploits conversion) *\) *)
-(* 	  w_unify_to_subterm ~flags:rewrite2_unif_flags *)
-(* 	    (pf_env gl) (c1,but) cl.evd *)
-(*   in *)
-(*   let cl' = {cl with evd = env' } in *)
-(*   let c2 = Clenv.clenv_nf_meta cl' c2 in *)
-(*   check_evar_map_of_evars_defs env' ; *)
-(*   env',Clenv.clenv_value cl', c1, c2 *)
-
+let convertible env evd x y =
+  Reductionops.is_trans_conv conv_transparent_state env (Evd.evars_of evd) x y
+  
 let allowK = true
 
 let refresh_hypinfo env sigma hypinfo = 
@@ -743,12 +659,7 @@ let unify_eqn env sigma hypinfo t =
       let left = if l2r then c1 else c2 in
 	match abs with
 	    Some _ -> 
-	      (* Disallow unfolding of a local var. *)
-	      if isVar left || isVar t then
-		if eq_constr left t then
-		  cl, c1, c2, car, rel
-		else raise Not_found
-	      else if convertible env cl.evd left t then
+	      if convertible env cl.evd left t then
 		cl, c1, c2, car, rel
 	      else raise Not_found
 	  | None ->
@@ -813,23 +724,6 @@ let unfold_all t =
 	  | _ -> assert false)
     | _ -> assert false
 
-(* let lift_cstr env sigma evars args cstr = *)
-(*   let codom =  *)
-(*     match cstr with *)
-(*       | Some c -> c *)
-(*       | None -> *)
-(* 	  let ty = Evarutil.e_new_evar evars env (new_Type ()) in *)
-(* 	  let rel = Evarutil.e_new_evar evars env (mk_relation ty) in *)
-(* 	    (ty, rel) *)
-(*   in *)
-(*     Array.fold_right *)
-(*       (fun arg (car, rel) ->  *)
-(* 	let ty = Typing.type_of env sigma arg in *)
-(* 	let car' = mkProd (Anonymous, ty, car) in *)
-(* 	let rel' = mkApp (Lazy.force pointwise_relation, [| ty; car; rel |]) in *)
-(* 	  (car', rel')) *)
-(*       args codom *)
-
 let rec decomp_pointwise n c =
   if n = 0 then c
   else
@@ -1498,17 +1392,11 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
   let prfty = Clenv.clenv_type cl' in
   let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
     {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
-(*         if occur_meta prf then *)
-(* else *)
-(*       {cl=cl'; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=None} *)
 
 let get_hyp gl c clause l2r = 
-(*   match kind_of_term (pf_type_of gl c) with *)
-(*       Prod _ ->  *)
-	let hi = decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r in
-	let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
-	  unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
-(*     | _ -> decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r *)
+  let hi = decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r in
+  let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
+    unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
 	
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
 
@@ -1556,9 +1444,6 @@ let setoid_reflexivity gl =
     with Not_found -> 
       tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared reflexive relation")
 	gl
-
-(* let setoid_reflexivity gl = *)
-(*   try_loaded setoid_reflexivity gl *)
 	  
 let setoid_symmetry gl =
   let env = pf_env gl in
@@ -1568,9 +1453,6 @@ let setoid_symmetry gl =
     with Not_found -> 
       tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared symmetric relation")
 	gl
-
-(* let setoid_symmetry gl = *)
-(*   try_loaded setoid_symmetry gl *)
 	
 let setoid_transitivity c gl =
   let env = pf_env gl in
@@ -1582,9 +1464,6 @@ let setoid_transitivity c gl =
     with Not_found -> 
       tclFAIL 0
 	(str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared transitive relation") gl
-	
-(* let setoid_transitivity c gl = *)
-(*   try_loaded (setoid_transitivity c) gl *)
 
 let setoid_symmetry_in id gl =
   let ctype = pf_type_of gl (mkVar id) in
@@ -1604,9 +1483,6 @@ let setoid_symmetry_in id gl =
 	tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ] ]
       gl
 
-(* let setoid_symmetry_in h gl = *)
-(*   try_loaded (setoid_symmetry_in h) gl *)
-
 let _ = Tactics.register_setoid_reflexivity setoid_reflexivity
 let _ = Tactics.register_setoid_symmetry setoid_symmetry
 let _ = Tactics.register_setoid_symmetry_in setoid_symmetry_in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 5c59e8244..0facf2393 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -103,7 +103,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
-	     (Hint_db.add_list hintl local_db) g'))) ::
+	     (add_hint_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 
@@ -112,16 +112,16 @@ 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 
-      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
+      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 (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
+      list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in 
   let tac_of_hint = 
-    fun {pri=b; pat = p; code=t} -> 
+    fun (st, {pri=b; pat = p; code=t}) -> 
       (b, 
        let tac =
 	 match t with
-	   | Res_pf (term,cl) -> unify_resolve (term,cl)
+	   | Res_pf (term,cl) -> unify_resolve st (term,cl)
 	   | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
 	   | Give_exact (c) -> e_give_exact_constr c
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
@@ -168,8 +168,8 @@ type search_state = {
   depth : int; (*r depth of search before failing *)
   tacres : goal list sigma * validation;
   last_tactic : std_ppcmds;
-  dblist : Auto.Hint_db.t list;
-  localdb :  Auto.Hint_db.t list }
+  dblist : Auto.hint_db list;
+  localdb :  Auto.hint_db list }
     
 module SearchProblem = struct
     
@@ -235,7 +235,7 @@ module SearchProblem = struct
 	       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
+             let ldb = add_hint_list hintl (List.hd s.localdb) in
 	     { depth = s.depth; tacres = res; 
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb })
@@ -255,7 +255,7 @@ module SearchProblem = struct
 	       { depth = pred s.depth; tacres = res; 
 		 dblist = s.dblist; last_tactic = pp;
 		 localdb = 
-		   list_addn (nbgl'-nbgl) (match s.localdb with [] -> assert false | hd :: _ -> hd) s.localdb })
+		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
 	  l
       in
       List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index d1883aa66..1c6f9920f 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -34,4 +34,4 @@ val gen_eauto : bool -> bool * int -> constr list ->
 val eauto_with_bases :
   bool ->
   bool * int ->
-  Term.constr list -> Auto.Hint_db.t list -> Proof_type.tactic
+  Term.constr list -> Auto.hint_db list -> Proof_type.tactic
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index e3c4e2649..b19df1aee 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1732,17 +1732,15 @@ let check_evar_map_of_evars_defs evd =
    returns the modified objects (in particular [c1] and [c2]) *)  
 
 let rewrite_unif_flags = {
-  modulo_conv_on_closed_terms = false;
+  modulo_conv_on_closed_terms = None;
   use_metas_eagerly = true;
-  modulo_delta = Cpred.empty;
-  modulo_zeta = false;
+  modulo_delta = empty_transparent_state;
 }
 
 let rewrite2_unif_flags = {
-  modulo_conv_on_closed_terms = true;
+  modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
-  modulo_delta = Cpred.empty;
-  modulo_zeta = false;
+  modulo_delta = empty_transparent_state;
 }
 
 let unification_rewrite c1 c2 cl but gl = 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9eec0c064..34c2f690c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -549,10 +549,9 @@ let last_arg c = match kind_of_term c with
   | _ -> anomaly "last_arg"
 
 let elim_flags = {
-  modulo_conv_on_closed_terms = true; 
+  modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = true;
-  modulo_delta = Cpred.empty;
-  modulo_zeta = true;
+  modulo_delta = empty_transparent_state;
 }
 
 let elimination_clause_scheme with_evars allow_K elimclause indclause gl =