- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence

  as hints (see wish #2104).
- New type hint_entry for interpreted hint.
- Better centralization of functions dealing with evaluable_global_reference.
- Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had
  uglily to be factorized by hand.
- Typography in RefMan-tac.tex.



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

21 files changed, 214 insertions, 128 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index c82e1e652f..92ea62b5e4 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,7 +2,7 @@
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
-** Cleaning in parsing extensions (commit )
+** Cleaning in parsing extensions (commit 12108)
 
 Many moves and renamings, one new file (Extrawit, that contains wit_tactic).
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4e31137c96..0a58cddfa0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3810,7 +3810,7 @@ where {\sl hint\_definition} is one of the following expressions:
 
   \end{Variants}
 
-\item \texttt{Transparent},\texttt{Opaque} {\qualid}
+\item \texttt{Transparent}, \texttt{Opaque} {\qualid}
 \label{HintTransparency}
 \comindex{Hint Transparent}
 \comindex{Hint Opaque}
@@ -3823,7 +3823,7 @@ where {\sl hint\_definition} is one of the following expressions:
   
   \begin{Variants}
 
-    \item \texttt{Transparent},\texttt{Opaque} {\ident$_1$} \dots {\ident$_m$} 
+    \item \texttt{Transparent}, \texttt{Opaque} {\ident$_1$} \dots {\ident$_m$} 
 
       Declares each {\ident$_i$} as a transparent or opaque constant.
       
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 43c7747077..087a519826 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -258,6 +258,10 @@ let coq_and = lazy_init_constant ["Logic"] "and"
 let coq_conj = lazy_init_constant ["Logic"] "conj"
 let coq_or = lazy_init_constant ["Logic"] "or"
 let coq_ex = lazy_init_constant ["Logic"] "ex"
+let coq_iff = lazy_init_constant ["Logic"] "iff"
+
+let coq_iff_left_proj  = lazy_init_constant ["Logic"] "proj1"
+let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2"
 
 (* Runtime part *)
 let build_coq_True ()  = Lazy.force coq_True
@@ -267,8 +271,13 @@ let build_coq_False () = Lazy.force coq_False
 let build_coq_not ()   = Lazy.force coq_not
 let build_coq_and ()   = Lazy.force coq_and
 let build_coq_conj ()  = Lazy.force coq_conj
-let build_coq_or ()   = Lazy.force coq_or
-let build_coq_ex ()   = Lazy.force coq_ex
+let build_coq_or ()    = Lazy.force coq_or
+let build_coq_ex ()    = Lazy.force coq_ex
+let build_coq_iff ()   = Lazy.force coq_iff
+
+let build_coq_iff_left_proj ()  = Lazy.force coq_iff_left_proj
+let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
+
 
 (* The following is less readable but does not depend on parsing *)
 let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
@@ -280,4 +289,5 @@ let coq_False_ref   = lazy (init_reference ["Logic"] "False")
 let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
 let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
 let coq_or_ref     = lazy (init_reference ["Logic"] "or")
+let coq_iff_ref    = lazy (init_reference ["Logic"] "iff")
 
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index a4751f6e79..7e13b1b1ed 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -137,6 +137,10 @@ val build_coq_not : constr delayed
 (* Conjunction *)
 val build_coq_and : constr delayed
 val build_coq_conj : constr delayed
+val build_coq_iff : constr delayed
+
+val build_coq_iff_left_proj : constr delayed
+val build_coq_iff_right_proj : constr delayed
 
 (* Disjunction *)
 val build_coq_or : constr delayed
@@ -154,3 +158,4 @@ val coq_sumbool_ref : global_reference lazy_t
 val coq_sig_ref : global_reference lazy_t
 
 val coq_or_ref : global_reference lazy_t
+val coq_iff_ref : global_reference lazy_t
diff --git a/lib/util.ml b/lib/util.ml
index 1014a6545c..82b1afabfb 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -49,6 +49,12 @@ exception Error_in_file of string * (bool * string * loc) * exn
 let on_fst f (a,b) = (f a,b)
 let on_snd f (a,b) = (a,f b)
 
+(* Mapping under pairs *)
+
+let on_pi1 f (a,b,c) = (f a,b,c)
+let on_pi2 f (a,b,c) = (a,f b,c)
+let on_pi3 f (a,b,c) = (a,b,f c)
+
 (* Projections from triplets *)
 
 let pi1 (a,_,_) = a
diff --git a/lib/util.mli b/lib/util.mli
index 0acff599db..04d3a52fcf 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -59,6 +59,12 @@ exception Error_in_file of string * (bool * string * loc) * exn
 val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
 
+(* Mapping under triple *)
+
+val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
+val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd
+val on_pi3 : ('a -> 'b) -> 'c * 'd * 'a -> 'c * 'd * 'b
+
 (*s Projections from triplets *)
 
 val pi1 : 'a * 'b * 'c -> 'a
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 0a486cb1e4..d4232eb959 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -93,10 +93,16 @@ GEXTEND Gram
       | IDENT "Create"; IDENT "HintDb" ; 
 	  id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
 	    VernacCreateHintDb (use_locality (), id, b)
-      | IDENT "Hint"; local = obsolete_locality; h = hint;
-        dbnames = opt_hintbases ->
+      | IDENT "Hint"; local = obsolete_locality; h = hint; 
+	  dbnames = opt_hintbases ->
 	  VernacHints (enforce_locality_of local,dbnames, h)
-	  
+
+(* Declare "Resolve" directly so as to be able to later extend with 
+   "Resolve ->" and "Resolve <-" *)
+      | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural; 
+	  dbnames = opt_hintbases ->
+	  VernacHints (enforce_locality_of false,dbnames,
+	    HintsResolve (List.map (fun x -> (n, true, x)) lc))
 
 (*This entry is not commented, only for debug*)
       | IDENT "PrintConstr"; c = constr -> 
@@ -108,7 +114,7 @@ GEXTEND Gram
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
   hint:
-    [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] -> 
+    [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT natural -> 
           HintsResolve (List.map (fun x -> (n, true, x)) lc)
       | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
       | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
diff --git a/parsing/printer.ml b/parsing/printer.ml
index f26d4d9cfc..267d550a97 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -114,10 +114,7 @@ let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
 let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
 
 let pr_evaluable_reference ref =
- let ref' = match ref with
-  | EvalConstRef const -> ConstRef const
-  | EvalVarRef sp -> VarRef sp in
- pr_global ref'
+  pr_global (Tacred.global_of_evaluable_reference ref)
 
 (*let pr_rawterm t =
   pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)*)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 55df4b185e..34187c919b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -35,15 +35,20 @@ exception ReductionTacticError of reduction_tactic_error
 exception Elimconst
 exception Redelimination
 
+let error_not_evaluable r =
+  errorlabstrm "error_not_evaluable"
+    (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Idset.empty r ++ 
+     spc () ++ str "to an evaluable reference.")
+
+let is_evaluable_const env cst =
+  is_transparent (ConstKey cst) && evaluable_constant cst env
+
+let is_evaluable_var env id =
+  is_transparent (VarKey id) && evaluable_named id env
+
 let is_evaluable env = function
-  | EvalConstRef kn ->
-      is_transparent (ConstKey kn) &&
-      let cb = Environ.lookup_constant kn env in
-      cb.const_body <> None & not cb.const_opaque
-  | EvalVarRef id ->
-      is_transparent (VarKey id) &&
-      let (_,value,_) = Environ.lookup_named id env in
-      value <> None
+  | EvalConstRef cst -> is_evaluable_const env cst
+  | EvalVarRef id -> is_evaluable_var env id
 
 let value_of_evaluable_ref env = function
   | EvalConstRef con -> constant_value env con
@@ -53,6 +58,15 @@ let constr_of_evaluable_ref = function
   | EvalConstRef con -> mkConst con
   | EvalVarRef id -> mkVar id
 
+let evaluable_of_global_reference env = function
+  | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst
+  | VarRef id when is_evaluable_var env id -> EvalVarRef id
+  | r -> error_not_evaluable r
+
+let global_of_evaluable_reference = function
+  | EvalConstRef cst -> ConstRef cst
+  | EvalVarRef id -> VarRef id
+
 type evaluable_reference =
   | EvalConst of constant
   | EvalVar of identifier
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 1516a2bd6a..c29a3f335a 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -26,7 +26,17 @@ exception ReductionTacticError of reduction_tactic_error
 
 (*s Reduction functions associated to tactics. \label{tacred} *)
 
-val is_evaluable : env -> evaluable_global_reference -> bool
+(* Evaluable global reference *)
+
+val is_evaluable : Environ.env -> evaluable_global_reference -> bool
+
+val error_not_evaluable : Libnames.global_reference -> 'a
+
+val evaluable_of_global_reference :
+  Environ.env -> Libnames.global_reference -> evaluable_global_reference
+
+val global_of_evaluable_reference :
+  evaluable_global_reference -> Libnames.global_reference
 
 exception Redelimination
 
@@ -75,7 +85,7 @@ val reduce_to_atomic_ind : env ->  evar_map -> types -> inductive * types
 val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 
 (* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
-   [t'=(x1:A1)..(xn:An)(ref args)] and raise [Not_found] if not possible *)
+   [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
 val reduce_to_quantified_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 907995c542..aceb5c5250 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -325,8 +325,8 @@ let make_resolve_hyp env sigma (hname,_,htyp) =
     | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
 
 (* REM : in most cases hintname = id *)
-let make_unfold (ref, eref) =
-  (Some ref,
+let make_unfold eref =
+  (Some (global_of_evaluable_reference eref),
    { pri = 4;
      pat = None;
      code = Unfold_nth eref })
@@ -522,57 +522,57 @@ let forward_intern_tac =
 
 let set_extern_intern_tac f = forward_intern_tac := f
 
-let add_hints local dbnames0 h =
-  let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in
-  let env = Global.env() and sigma = Evd.empty in
-  let f = Constrintern.interp_constr sigma env in
+type hints_entry =
+  | HintsResolveEntry of (int option * bool * constr) list
+  | HintsImmediateEntry of constr list
+  | HintsUnfoldEntry of evaluable_global_reference list
+  | HintsTransparencyEntry of evaluable_global_reference list * bool
+  | HintsExternEntry of 
+      int * (patvar list * constr_pattern) option * glob_tactic_expr
+  | HintsDestructEntry of identifier * int * (bool,unit) location * 
+      (patvar list * constr_pattern) * glob_tactic_expr
+
+let interp_hints h =
+  let f = Constrintern.interp_constr Evd.empty (Global.env()) in
+  let fr r =
+    let gr = Syntax_def.global_with_alias r in
+    let r' = evaluable_of_global_reference (Global.env()) gr in
+    Dumpglob.add_glob (loc_of_reference r) gr;
+    r' in
+  let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
   match h with
-  | HintsResolve lhints ->	
-      add_resolves env sigma (List.map (fun (pri, b, x) -> pri, b, f x) lhints) local dbnames
-  | HintsImmediate lhints ->
-      add_trivials env sigma (List.map f lhints) local dbnames
-  | HintsUnfold lhints ->
-      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;
-	 (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
+  | HintsResolve lhints -> HintsResolveEntry (List.map (on_pi3 f) lhints)
+  | HintsImmediate lhints -> HintsImmediateEntry (List.map f lhints)
+  | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
+  | HintsTransparency (lhints, b) ->
+      HintsTransparencyEntry (List.map fr lhints, b)
   | HintsConstructors lqid ->
-      let add_one qid =
-        let env = Global.env() and sigma = Evd.empty in
+      let constr_hints_of_ind qid =
         let isp = inductive_of_reference qid in
         let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
-        let lcons = list_tabulate
-          (fun i -> None, true, mkConstruct (isp,i+1)) (Array.length consnames) in
-        add_resolves env sigma lcons local dbnames in
-      List.iter add_one lqid
+        list_tabulate (fun i -> None, true, mkConstruct (isp,i+1))
+	  (Array.length consnames) in
+	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
-      let pat =	Option.map (Constrintern.intern_constr_pattern Evd.empty (Global.env())) patcom in
+      let pat =	Option.map fp patcom in
       let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in
-      add_externs pri pat tacexp local dbnames
+      HintsExternEntry (pri, pat, tacexp)
   | HintsDestruct(na,pri,loc,pat,code) ->
+      let (l,_ as pat) = fp pat in
+      HintsDestructEntry (na,pri,loc,pat,!forward_intern_tac l code)
+
+let add_hints local dbnames0 h =
+  let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in
+  let env = Global.env() and sigma = Evd.empty in
+  match h with
+  | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
+  | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
+  | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
+  | HintsTransparencyEntry (lhints, b) ->
+      add_transparency lhints b local dbnames
+  | HintsExternEntry (pri, pat, tacexp) ->
+      add_externs pri pat tacexp local dbnames
+  | HintsDestructEntry (na,pri,loc,pat,code) ->
       if dbnames0<>[] then
         warn (str"Database selection not implemented for destruct hints");
       Dhyp.add_destructor_hint local na loc pat pri code
diff --git a/tactics/auto.mli b/tactics/auto.mli
index f893c9b15f..982a4e68ec 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -69,6 +69,16 @@ type hint_db_name = string
 
 type hint_db = Hint_db.t
 
+type hints_entry =
+  | HintsResolveEntry of (int option * bool * constr) list
+  | HintsImmediateEntry of constr list
+  | HintsUnfoldEntry of evaluable_global_reference list
+  | HintsTransparencyEntry of evaluable_global_reference list * bool
+  | HintsExternEntry of 
+      int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
+  | HintsDestructEntry of identifier * int * (bool,unit) Tacexpr.location * 
+      (patvar list * constr_pattern) * Tacexpr.glob_tactic_expr
+
 val searchtable_map : hint_db_name -> hint_db
 
 val searchtable_add : (hint_db_name * hint_db) -> unit
@@ -82,7 +92,9 @@ val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
 
 val current_db_names : unit -> hint_db_name list
 
-val add_hints : locality_flag -> hint_db_name list -> hints -> unit
+val interp_hints : hints_expr -> hints_entry
+
+val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
 val print_searchtable : unit -> unit
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 890f3a086e..e09ba93f8e 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -480,13 +480,15 @@ let _ =
     
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
 | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
-    add_hints false [typeclasses_db] (Vernacexpr.HintsTransparency (cl, true))
+    add_hints false [typeclasses_db]
+      (interp_hints (Vernacexpr.HintsTransparency (cl, true)))
   ]
 END
 	
 VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings
 | [ "Typeclasses" "Opaque" reference_list(cl) ] -> [
-    add_hints false [typeclasses_db] (Vernacexpr.HintsTransparency (cl, false))
+    add_hints false [typeclasses_db]
+      (interp_hints (Vernacexpr.HintsTransparency (cl, false)))
   ]
 END
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index b37212d9d6..3d34a2d688 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -225,16 +225,10 @@ let (inDD,_) =
 		    classify_function = classify_dd;
                     export_function = export_dd }
 
-let forward_intern_tac = 
-  ref (fun _ -> failwith "intern_tac is not installed for DHyp")
-
-let set_extern_intern_tac f = forward_intern_tac := f
-
 let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT"))
 let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE"))
     
-let add_destructor_hint local na loc pat pri code =
-  let code = !forward_intern_tac code in
+let add_destructor_hint local na loc (_,pat) pri code =
   let code =
     begin match loc, code with
       | HypLocation _, TacFun ([id],body) -> (id,body)
@@ -243,8 +237,6 @@ let add_destructor_hint local na loc pat pri code =
 	  errorlabstrm "add_destructor_hint"
           (str "The tactic should be a function of the hypothesis name.") end
   in
-  let (_,pat) = Constrintern.intern_constr_pattern Evd.empty (Global.env()) pat
-  in
   let pat = match loc with
     | HypLocation b ->
 	HypLocation
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index c86102e935..3277fd2e67 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -17,7 +17,6 @@ open Tacexpr
 (* Programmable destruction of hypotheses and conclusions. *)
 
 val set_extern_interp : (glob_tactic_expr -> tactic) -> unit
-val set_extern_intern_tac : (raw_tactic_expr -> glob_tactic_expr) -> unit
 
 (*
 val dHyp : identifier -> tactic
@@ -29,4 +28,5 @@ val h_auto_tdb : int option -> tactic
 
 val add_destructor_hint :
   Vernacexpr.locality_flag -> identifier -> (bool,unit) Tacexpr.location ->
-    Topconstr.constr_expr -> int -> raw_tactic_expr -> unit
+    Rawterm.patvar list * Pattern.constr_pattern -> int -> 
+      glob_tactic_expr -> unit
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 28e3888453..6bf3e34b02 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -204,6 +204,47 @@ VERNAC COMMAND EXTEND HintRewrite
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
     ":" preident(b) ] ->
   [ add_rewrite_hint b o t l ]
+| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
+  [ add_rewrite_hint "core" o (Tacexpr.TacId []) l ]
+| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
+  [ add_rewrite_hint "core" o t l ]
+END
+
+open Term
+open Coqlib
+
+let project_hint pri l2r c =
+  let env = Global.env() in
+  let c = Constrintern.interp_constr Evd.empty env c in
+  let t = Retyping.get_type_of env Evd.empty c in
+  let t = 
+    Tacred.reduce_to_quantified_ref env Evd.empty (Lazy.force coq_iff_ref) t in
+  let sign,ccl = decompose_prod_assum t in
+  let (a,b) = match snd (decompose_app ccl) with
+    | [a;b] -> (a,b)
+    | _ -> assert false in
+  let p =
+    if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
+  let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in
+  let c = it_mkLambda_or_LetIn
+    (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
+  (pri,true,c)
+
+let add_hints_iff l2r lc n bl =
+  Auto.add_hints true bl
+    (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc))
+
+VERNAC COMMAND EXTEND HintResolveIff
+  [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n)
+    ":" preident_list(bl) ] ->
+  [ add_hints_iff true lc n bl ]
+| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n)
+    ":" preident_list(bl) ] ->
+  [ add_hints_iff false lc n bl ]
+| [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ] ->
+  [ add_hints_iff true lc n ["core"] ]
+| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) ] ->
+  [ add_hints_iff false lc n ["core"] ]
 END
 
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 88692a13c5..8236f3e9e5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -174,11 +174,6 @@ let find_reference env qid =
 	-> VarRef id
     | _ -> Nametab.locate qid
 
-let error_not_evaluable s =
-  errorlabstrm "evalref_of_ref" 
-    (str "Cannot coerce" ++ spc ()  ++ s ++ spc () ++
-     str "to an evaluable reference.")
-
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 let atomic_mactab = ref Idmap.empty
 let add_primitive_tactic s tac =
@@ -315,23 +310,23 @@ let coerce_to_tactic loc id = function
 
 (* We have identifier <| global_reference <| constr *)
 
-let find_ident id sign = 
-  List.mem id (fst sign.ltacvars) or 
-  List.mem id (ids_of_named_context (Environ.named_context sign.genv))
+let find_ident id ist = 
+  List.mem id (fst ist.ltacvars) or 
+  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
-let find_recvar qid sign = List.assoc qid sign.ltacrecvars
+let find_recvar qid ist = List.assoc qid ist.ltacrecvars
 
 (* a "var" is a ltac var or a var introduced by an intro tactic *)
-let find_var id sign = List.mem id (fst sign.ltacvars)
+let find_var id ist = List.mem id (fst ist.ltacvars)
 
 (* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *)
-let find_ctxvar id sign = List.mem id (snd sign.ltacvars)
+let find_ctxvar id ist = List.mem id (snd ist.ltacvars)
 
 (* a "ltacvar" is an ltac var (Let-In/Fun/...) *)
-let find_ltacvar id sign = find_var id sign & not (find_ctxvar id sign)
+let find_ltacvar id ist = find_var id ist & not (find_ctxvar id ist)
 
-let find_hyp id sign =
-  List.mem id (ids_of_named_context (Environ.named_context sign.genv))
+let find_hyp id ist =
+  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
 (* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *)
 (* be fresh in which case it is binding later on *)
@@ -549,11 +544,6 @@ let intern_induction_arg ist = function
       else
 	ElimOnIdent (loc,id)
 
-let evaluable_of_global_reference = function
-  | ConstRef c -> EvalConstRef c
-  | VarRef c -> EvalVarRef c
-  | r -> error_not_evaluable (pr_global r)
-
 let short_name = function
   | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
   | _ -> None
@@ -566,21 +556,21 @@ let interp_global_reference r =
   | Ident (loc,id) when not !strict_check -> VarRef id
   | _ -> error_global_not_found_loc lqid
 
-let intern_evaluable_reference_or_by_notation = function
-  | AN r -> evaluable_of_global_reference (interp_global_reference r)
+let intern_evaluable_reference_or_by_notation ist = function
+  | AN r -> evaluable_of_global_reference ist.genv (interp_global_reference r)
   | ByNotation (loc,ntn,sc) ->
-      evaluable_of_global_reference
+      evaluable_of_global_reference ist.genv
       (Notation.interp_notation_as_global_reference loc
         (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
-(* Globalizes a reduction expression *)
+(* Globalize a reduction expression *)
 let intern_evaluable ist = function
   | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id)
   | AN (Ident (_,id)) when
       (not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
       ArgArg (EvalVarRef id, None)
   | r ->
-      let e = intern_evaluable_reference_or_by_notation r in
+      let e = intern_evaluable_reference_or_by_notation ist r in
       let na = short_name r in
       ArgArg (e,na)
 
@@ -1331,7 +1321,7 @@ let interp_evaluable ist env = function
       (* Maybe [id] has been introduced by Intro-like tactics *)
       (try match Environ.lookup_named id env with
        | (_,Some _,_) -> EvalVarRef id
-       | _ -> error_not_evaluable (pr_id id)
+       | _ -> error_not_evaluable (VarRef id)
        with Not_found ->
        match r with
        | EvalConstRef _ -> r
@@ -2951,5 +2941,3 @@ let _ = Auto.set_extern_intern_tac
     (intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
 let _ = Auto.set_extern_subst_tactic subst_tactic
 let _ = Dhyp.set_extern_interp eval_tactic
-let _ = Dhyp.set_extern_intern_tac
-  (fun t -> intern_tactic (make_empty_glob_sign()) t)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index e5c3322a35..2d5cd659f7 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -34,16 +34,13 @@ open Entries
 
 let typeclasses_db = "typeclass_instances"
 
-let qualid_of_con c = 
-  Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
-
 let _ =
   Typeclasses.register_add_instance_hint 
     (fun inst pri ->
       Flags.silently (fun () ->      
 	Auto.add_hints false [typeclasses_db] 
-	  (Vernacexpr.HintsResolve 
-	      [pri, false, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ())
+	  (Auto.HintsResolveEntry
+	      [pri, false, mkConst inst])) ())
     
 let declare_instance_cst glob con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b1a56d577c..3747dbc2a5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -291,7 +291,7 @@ let qualid_of_con c =
 
 let set_rigid c = 
   Auto.add_hints false [typeclasses_db] 
-    (Vernacexpr.HintsTransparency ([qualid_of_con c], false))
+    (Auto.HintsTransparencyEntry ([EvalConstRef c], false))
 
 let declare_instance_cst glob con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5d886c07e6..826b0364e4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -758,7 +758,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 let vernac_create_hintdb local id b = 
   Auto.create_hint_db local id full_transparent_state b
 
-let vernac_hints = Auto.add_hints
+let vernac_hints local lb h = Auto.add_hints local lb (Auto.interp_hints h)
 
 let vernac_syntactic_definition lid =
   Dumpglob.dump_definition lid false "syndef";
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 47b36ede0f..b38277cca1 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -110,7 +110,7 @@ type comment =
   | CommentString of string
   | CommentInt of int
 
-type hints =
+type hints_expr =
   | HintsResolve of (int option * bool * constr_expr) list
   | HintsImmediate of constr_expr list
   | HintsUnfold of reference list
@@ -124,15 +124,6 @@ type search_restriction =
   | SearchInside of reference list
   | SearchOutside of reference list
 
-type option_value =
-  | StringValue of string
-  | IntValue of int
-  | BoolValue of bool
-
-type option_ref_value =
-  | StringRefValue of string
-  | QualidRefValue of reference
-
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type opacity_flag   = bool (* true = Opaque;        false = Transparent    *)
@@ -144,6 +135,15 @@ type inductive_flag = Decl_kinds.recursivity_kind
 type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
 
+type option_value =
+  | StringValue of string
+  | IntValue of int
+  | BoolValue of bool
+
+type option_ref_value =
+  | StringRefValue of string
+  | QualidRefValue of reference
+
 type sort_expr = Rawterm.rawsort
 
 type definition_expr =
@@ -301,7 +301,7 @@ type vernac_expr =
   | VernacDeclareTacticDefinition of
       rec_flag * (reference * bool * raw_tactic_expr) list
   | VernacCreateHintDb of locality_flag * lstring * bool
-  | VernacHints of locality_flag * lstring list * hints
+  | VernacHints of locality_flag * lstring list * hints_expr
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * lreference *