Merge branch 'v8.6'

7 files changed, 178 insertions, 101 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 63f85114ee..d4251555d8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -34,6 +34,10 @@ open Hints
 
 let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
 
+let compute_secvars gl =
+  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+  secvars_of_hyps hyps
+
 (* tell auto not to reuse already instantiated metas in unification (for
    compatibility, since otherwise, apply succeeds oftener) *)
 
@@ -259,19 +263,19 @@ let pr_info_atom (d,pp) =
 
 let pr_info_trace = function
   | (Info,_,{contents=(d,Some pp)::l}) ->
-      Feedback.msg_debug (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l))
+      Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l))
   | _ -> ()
 
 let pr_info_nop = function
-  | (Info,_,_) -> Feedback.msg_debug (str "idtac.")
+  | (Info,_,_) -> Feedback.msg_info (str "idtac.")
   | _ -> ()
 
 let pr_dbg_header = function
   | (Off,_,_) -> ()
   | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
   | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
-  | (Info,0,_) -> Feedback.msg_debug (str "(* info trivial: *)")
-  | (Info,_,_) -> Feedback.msg_debug (str "(* info auto: *)")
+  | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)")
+  | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)")
 
 let tclTRY_dbg d tac =
   let delay f = Proofview.tclUNIT () >>= fun () -> f () in
@@ -294,12 +298,13 @@ let flags_of_state st =
 let auto_flags_of_state st =
   auto_unif_flags_of full_transparent_state st false
 
-let hintmap_of hdc concl =
+let hintmap_of secvars hdc concl =
   match hdc with
-  | None -> Hint_db.map_none
+  | None -> Hint_db.map_none ~secvars
   | Some hdc ->
-      if occur_existential concl then Hint_db.map_existential hdc concl
-      else Hint_db.map_auto hdc concl
+     if occur_existential concl then
+       Hint_db.map_existential ~secvars hdc concl
+     else Hint_db.map_auto ~secvars hdc concl
 
 let exists_evaluable_reference env = function
   | EvalConstRef _ -> true
@@ -324,22 +329,23 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
   in
   Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Tacmach.New.pf_nf_concl gl in
+    let secvars = compute_secvars gl in
     Tacticals.New.tclFIRST
       ((dbg_assumption dbg)::intro_tac::
           (List.map Tacticals.New.tclCOMPLETE
-             (trivial_resolve dbg mod_delta db_list local_db concl)))
+             (trivial_resolve dbg mod_delta db_list local_db secvars concl)))
   end }
 
-and my_find_search_nodelta db_list local_db hdc concl =
+and my_find_search_nodelta db_list local_db secvars hdc concl =
   List.map (fun hint -> (None,hint))
-    (List.map_append (hintmap_of hdc concl) (local_db::db_list))
+    (List.map_append (hintmap_of secvars hdc concl) (local_db::db_list))
 
 and my_find_search mod_delta =
   if mod_delta then my_find_search_delta
   else my_find_search_nodelta
 
-and my_find_search_delta db_list local_db hdc concl =
-  let f = hintmap_of hdc concl in
+and my_find_search_delta db_list local_db secvars hdc concl =
+  let f = hintmap_of secvars hdc concl in
     if occur_existential concl then
       List.map_append
 	(fun db ->
@@ -359,11 +365,11 @@ and my_find_search_delta db_list local_db hdc concl =
 	  let (ids, csts as st) = Hint_db.transparent_state db in
 	  let flags, l =
 	    let l =
-	      match hdc with None -> Hint_db.map_none db
+	      match hdc with None -> Hint_db.map_none ~secvars db
 	      | Some hdc ->
 		  if (Id.Pred.is_empty ids && Cpred.is_empty csts)
-		  then Hint_db.map_auto hdc concl db
-		  else Hint_db.map_existential hdc concl db
+		  then Hint_db.map_auto ~secvars hdc concl db
+		  else Hint_db.map_existential ~secvars hdc concl db
 	    in auto_flags_of_state st, l
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
@@ -396,7 +402,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
   in
   tclLOG dbg pr_hint (run_hint t tactic)
 
-and trivial_resolve dbg mod_delta db_list local_db cl =
+and trivial_resolve dbg mod_delta db_list local_db secvars cl =
   try
     let head =
       try let hdconstr = decompose_app_bound cl in
@@ -405,7 +411,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
     in
       List.map (tac_of_hint dbg db_list local_db cl)
 	(priority
-	    (my_find_search mod_delta db_list local_db head cl))
+	    (my_find_search mod_delta db_list local_db secvars head cl))
   with Not_found -> []
 
 (** The use of the "core" database can be de-activated by passing
@@ -443,7 +449,7 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
 (*                       The classical Auto tactic                        *)
 (**************************************************************************)
 
-let possible_resolve dbg mod_delta db_list local_db cl =
+let possible_resolve dbg mod_delta db_list local_db secvars cl =
   try
     let head =
       try let hdconstr = decompose_app_bound cl in
@@ -451,7 +457,7 @@ let possible_resolve dbg mod_delta db_list local_db cl =
       with Bound -> None
     in
       List.map (tac_of_hint dbg db_list local_db cl)
-	(my_find_search mod_delta db_list local_db head cl)
+	(my_find_search mod_delta db_list local_db secvars head cl)
   with Not_found -> []
 
 let extend_local_db decl db gl =
@@ -482,11 +488,12 @@ let search d n mod_delta db_list local_db =
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
 	     ( Proofview.Goal.enter { enter = begin fun gl ->
                let concl = Tacmach.New.pf_nf_concl gl in
+               let secvars = compute_secvars gl in
 	       let d' = incr_dbg d in
 	       Tacticals.New.tclFIRST
 	         (List.map
 		    (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
-		    (possible_resolve d mod_delta db_list local_db concl))
+		    (possible_resolve d mod_delta db_list local_db secvars concl))
              end }))
     end []
   in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 3ee96353f1..06048ac1c5 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -16,6 +16,8 @@ open Decl_kinds
 open Hints
 open Tactypes
 
+val compute_secvars : ('a,'b) Proofview.Goal.t -> Id.Pred.t
+
 val default_search_depth : int ref
 
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 96767e7f62..a4243164ed 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -282,11 +282,11 @@ let clenv_of_prods poly nprods (c, clenv) gl =
     let ty = Retyping.get_type_of (Proofview.Goal.env gl)
                                   (Sigma.to_evar_map (Proofview.Goal.sigma gl)) c in
     let diff = nb_prod ty - nprods in
-      if Pervasives.(>=) diff 0 then
-        (* Was Some clenv... *)
-        Some (Some diff,
-              Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
-      else None
+    if Pervasives.(>=) diff 0 then
+      (* Was Some clenv... *)
+      Some (Some diff,
+            Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
+    else None
 
 let with_prods nprods poly (c, clenv) f =
   if get_typeclasses_limit_intros () then
@@ -341,7 +341,7 @@ let shelve_dependencies gls =
    shelve_goals gls)
 
 (** Hack to properly solve dependent evars that are typeclasses *)
-let rec e_trivial_fail_db only_classes db_list local_db =
+let rec e_trivial_fail_db only_classes db_list local_db secvars =
   let open Tacticals.New in
   let open Tacmach.New in
   let trivial_fail =
@@ -352,13 +352,13 @@ let rec e_trivial_fail_db only_classes db_list local_db =
     let d = pf_last_hyp gl in
     let hintl = make_resolve_hyp env sigma d in
     let hints = Hint_db.add_list env sigma hintl local_db in
-      e_trivial_fail_db only_classes db_list hints
+      e_trivial_fail_db only_classes db_list hints secvars
       end }
   in
   let trivial_resolve =
     Proofview.Goal.nf_enter { enter =
     begin fun gl ->
-    let tacs = e_trivial_resolve db_list local_db only_classes
+    let tacs = e_trivial_resolve db_list local_db secvars only_classes
                                  (project gl) (pf_concl gl) in
       tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs)
     end}
@@ -369,7 +369,7 @@ let rec e_trivial_fail_db only_classes db_list local_db =
   in
   tclFIRST (List.map tclCOMPLETE tacl)
 
-and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
+and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl =
   let open Proofview.Notations in
   let prods, concl = decompose_prod_assum concl in
   let nprods = List.length prods in
@@ -386,15 +386,15 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
       (fun db ->
         let tacs =
           if Hint_db.use_dn db then (* Using dnet *)
-            Hint_db.map_eauto hdc concl db
-          else Hint_db.map_existential hdc concl db
+            Hint_db.map_eauto secvars hdc concl db
+          else Hint_db.map_existential secvars hdc concl db
         in
         let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
           List.map (fun x -> (flags, x)) tacs)
       (local_db::db_list)
   in
   let tac_of_hint =
-    fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
+    fun (flags, {pri = b; pat = p; poly = poly; code = t; secvars; name = name}) ->
       let tac = function
         | Res_pf (term,cl) ->
            if get_typeclasses_filtered_unification () then
@@ -431,7 +431,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
       | Res_pf_THEN_trivial_fail (term,cl) ->
          let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
          let snd = if complete then Tacticals.New.tclIDTAC
-                   else e_trivial_fail_db only_classes db_list local_db in
+                   else e_trivial_fail_db only_classes db_list local_db secvars in
          Tacticals.New.tclTHEN fst snd
       | Unfold_nth c ->
          let tac = Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]) in
@@ -451,15 +451,15 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
         | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp))
   in List.map tac_of_hint hintl
 
-and e_trivial_resolve db_list local_db only_classes sigma concl =
+and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
   try
-    e_my_find_search db_list local_db
+    e_my_find_search db_list local_db secvars
      (decompose_app_bound concl) true only_classes sigma concl
   with Bound | Not_found -> []
 
-let e_possible_resolve db_list local_db only_classes sigma concl =
+let e_possible_resolve db_list local_db secvars only_classes sigma concl =
   try
-    e_my_find_search db_list local_db
+    e_my_find_search db_list local_db secvars
       (decompose_app_bound concl) false only_classes sigma concl
   with Bound | Not_found -> []
 
@@ -673,7 +673,8 @@ module V85 = struct
     let env = Goal.V82.env s gl in
     let concl = Goal.V82.concl s gl in
     let tacgl = {it = gl; sigma = s;} in
-    let poss = e_possible_resolve hints info.hints info.only_classes s concl in
+    let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in
+    let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in
     let unique = is_unique env concl in
     let rec aux i foundone = function
       | (tac, _, extern, name, pp) :: tl ->
@@ -1004,8 +1005,9 @@ module Search = struct
            Printer.pr_constr_env (Goal.env gl) s concl ++
            (if backtrack then str" with backtracking"
             else str" without backtracking"));
+    let secvars = compute_secvars gl in
     let poss =
-      e_possible_resolve hints info.search_hints info.search_only_classes s concl in
+      e_possible_resolve hints info.search_hints secvars info.search_only_classes s concl in
     (* If no goal depends on the solution of this one or the
        instances are irrelevant/assumed to be unique, then
        we don't need to backtrack, as long as no evar appears in the goal
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index c6b7de32d1..10c975b8d8 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -119,12 +119,13 @@ let unify_e_resolve poly flags (c,clenv) =
 		 (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
     end }
 
-let hintmap_of hdc concl =
+let hintmap_of secvars hdc concl =
   match hdc with
-  | None -> fun db -> Hint_db.map_none db
+  | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
-    if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db)
-    else (fun db -> Hint_db.map_auto hdc concl db)
+     if occur_existential concl then
+       (fun db -> Hint_db.map_existential ~secvars hdc concl db)
+     else (fun db -> Hint_db.map_auto ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
 let e_exact poly flags (c,clenv) =
@@ -142,16 +143,17 @@ let rec e_trivial_fail_db db_list local_db =
     e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
   end } in
   Proofview.Goal.enter { enter = begin fun gl ->
+  let secvars = compute_secvars gl in
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl)))
+    (List.map fst (e_trivial_resolve db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end }
 
-and e_my_find_search db_list local_db hdc concl =
-  let hint_of_db = hintmap_of hdc concl in
+and e_my_find_search db_list local_db secvars hdc concl =
+  let hint_of_db = hintmap_of secvars hdc concl in
   let hintl =
       List.map_append (fun db ->
 	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
@@ -179,14 +181,15 @@ and e_my_find_search db_list local_db hdc concl =
   in
   List.map tac_of_hint hintl
 
-and e_trivial_resolve db_list local_db gl =
+and e_trivial_resolve db_list local_db secvars gl =
   let hd = try Some (decompose_app_bound gl) with Bound -> None in
-  try priority (e_my_find_search db_list local_db hd gl)
+  try priority (e_my_find_search db_list local_db secvars hd gl)
   with Not_found -> []
 
-let e_possible_resolve db_list local_db gl =
+let e_possible_resolve db_list local_db secvars gl =
   let hd = try Some (decompose_app_bound gl) with Bound -> None in
-  try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl)
+  try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
+               (e_my_find_search db_list local_db secvars hd gl)
   with Not_found -> []
 
 let find_first_goal gls =
@@ -255,9 +258,11 @@ module SearchProblem = struct
       let nbgl = List.length (sig_it lg) in
       assert (nbgl > 0);
       let g = find_first_goal lg in
+      let hyps = pf_ids_of_hyps g in
+      let secvars = secvars_of_hyps (pf_hyps g) in
       let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
       let assumption_tacs =
-        let tacs = List.map map_assum (pf_ids_of_hyps g) in
+        let tacs = List.map map_assum hyps in
         let l = filter_tactics s.tacres tacs in
 	List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
 				    last_tactic = pp; dblist = s.dblist;
@@ -283,7 +288,8 @@ module SearchProblem = struct
       let rec_tacs =
 	let l =
           let concl = Reductionops.nf_evar (project g)(pf_concl g) in
-	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) concl)
+	  filter_tactics s.tacres
+                         (e_possible_resolve s.dblist (List.hd s.localdb) secvars concl)
 	in
 	List.map
 	  (fun (lgls, cost, pp) ->
@@ -346,13 +352,13 @@ let mk_eauto_dbg d =
   else Off
 
 let pr_info_nop = function
-  | Info -> Feedback.msg_debug (str "idtac.")
+  | Info -> Feedback.msg_info (str "idtac.")
   | _ -> ()
 
 let pr_dbg_header = function
   | Off -> ()
   | Debug -> Feedback.msg_debug (str "(* debug eauto: *)")
-  | Info  -> Feedback.msg_debug (str "(* info eauto: *)")
+  | Info  -> Feedback.msg_info (str "(* info eauto: *)")
 
 let pr_info dbg s =
   if dbg != Info then ()
@@ -363,7 +369,7 @@ let pr_info dbg s =
 	| State sp ->
 	  let mindepth = loop sp in
 	  let indent = String.make (mindepth - sp.depth) ' ' in
-	  Feedback.msg_debug (str indent ++ Lazy.force s.last_tactic ++ str ".");
+	  Feedback.msg_info (str indent ++ Lazy.force s.last_tactic ++ str ".");
 	  mindepth
     in
     ignore (loop s)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3d5be5441c..9fa49264fe 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -69,6 +69,25 @@ let decompose_app_bound t =
     | Proj (p, c) -> ConstRef (Projection.constant p), Array.cons c args
     | _ -> raise Bound
 
+(** Compute the set of section variables that remain in the named context.
+    Starts from the top to the bottom of the context, stops at the first
+    different declaration between the named hyps and the section context. *)
+let secvars_of_hyps hyps =
+  let secctx = Global.named_context () in
+  let open Context.Named.Declaration in
+  let pred, all =
+    List.fold_left (fun (pred,all) decl ->
+        try let _ = Context.Named.lookup (get_id decl) hyps in
+          (* Approximation, it might be an hypothesis reintroduced with same name and unconvertible types,
+             we must allow it currently, as comparing the declarations for syntactic equality is too
+             strong a check (e.g. an unfold in a section variable would make it unusable). *)
+          (Id.Pred.add (get_id decl) pred, all)
+        with Not_found -> (pred, false))
+      (Id.Pred.empty,true) secctx
+  in
+  if all then Id.Pred.full (* If the whole section context is available *)
+  else pred
+
 (************************************************************************)
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
@@ -107,12 +126,13 @@ type raw_hint = constr * types * Univ.universe_context_set
 type hint = (raw_hint * clausenv) hint_ast with_uid
 
 type 'a with_metadata = {
-  pri  : int;            (* A number lower is higher priority *)
-  poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
-  pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
-  name  : hints_path_atom; (* A potential name to refer to the hint *) 
+  pri     : int;            (* A number lower is higher priority *)
+  poly    : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
+  pat     : constr_pattern option; (* A pattern for the concl of the Goal *)
+  name    : hints_path_atom; (* A potential name to refer to the hint *)
   db : string option; (** The database from which the hint comes *)
-  code : 'a;     (* the tactic to apply when the concl matches pat *)
+  secvars : Id.Pred.t; (* The set of section variables the hint depends on *)
+  code    : 'a;     (* the tactic to apply when the concl matches pat *)
 }
 
 type full_hint = hint with_metadata
@@ -421,11 +441,14 @@ sig
 type t
 val empty : ?name:hint_db_name -> transparent_state -> bool -> t
 val find : global_reference -> t -> search_entry
-val map_none : t -> full_hint list
-val map_all : global_reference -> t -> full_hint list
-val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list
-val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list
-val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
+val map_none : secvars:Id.Pred.t -> t -> full_hint list
+val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+val map_existential : secvars:Id.Pred.t ->
+		      (global_reference * constr array) -> constr -> t -> full_hint list
+val map_eauto : secvars:Id.Pred.t ->
+		(global_reference * constr array) -> constr -> t -> full_hint list
+val map_auto : secvars:Id.Pred.t ->
+	       (global_reference * constr array) -> constr -> t -> full_hint list
 val add_one : env -> evar_map -> hint_entry -> t -> t
 val add_list : env -> evar_map -> hint_entry list -> t -> t
 val remove_one : global_reference -> t -> t
@@ -474,7 +497,11 @@ struct
     try Constr_map.find key db.hintdb_map
     with Not_found -> empty_se
  
-  let realize_tac (id,tac) = tac
+  let realize_tac secvars (id,tac) =
+    if Id.Pred.subset tac.secvars secvars then Some tac
+    else
+      (** Warn about no longer typable hint? *)
+      None
 
   let match_mode m arg =
     match m with
@@ -492,40 +519,40 @@ struct
     if List.is_empty modes then true
     else List.exists (matches_mode args) modes
 
-  let merge_entry db nopat pat =
+  let merge_entry secvars db nopat pat =
     let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in
     let h = List.merge pri_order_int h nopat in
     let h = List.merge pri_order_int h pat in
-    List.map realize_tac h
+    List.map_filter (realize_tac secvars) h
 
-  let map_none db =
-    merge_entry db [] []
+  let map_none ~secvars db =
+    merge_entry secvars db [] []
 
-  let map_all k db =
+  let map_all ~secvars k db =
     let se = find k db in
-    merge_entry db se.sentry_nopat se.sentry_pat
+    merge_entry secvars db se.sentry_nopat se.sentry_pat
 	
   (** Precondition: concl has no existentials *)
-  let map_auto (k,args) concl db =
+  let map_auto ~secvars (k,args) concl db =
     let se = find k db in
     let st = if db.use_dn then  (Some db.hintdb_state) else None in
     let pat = lookup_tacs concl st se in
-    merge_entry db [] pat
+    merge_entry secvars db [] pat
 
-  let map_existential (k,args) concl db =
+  let map_existential ~secvars (k,args) concl db =
     let se = find k db in
       if matches_modes args se.sentry_mode then
-        merge_entry db se.sentry_nopat se.sentry_pat
-      else merge_entry db [] []
+        merge_entry secvars db se.sentry_nopat se.sentry_pat
+      else merge_entry secvars db [] []
 
   (* [c] contains an existential *)
-  let map_eauto (k,args) concl db =
+  let map_eauto ~secvars (k,args) concl db =
     let se = find k db in
       if matches_modes args se.sentry_mode then
         let st = if db.use_dn then Some db.hintdb_state else None in
         let pat = lookup_tacs concl st se in
-        merge_entry db [] pat
-      else merge_entry db [] []
+        merge_entry secvars db [] pat
+      else merge_entry secvars db [] []
 
   let is_exact = function
     | Give_exact _ -> true
@@ -601,11 +628,11 @@ struct
 
   let get_entry se =
     let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in
-    List.map realize_tac h
+    List.map snd h
 
   let iter f db =
     let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
-    f None [] (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat);
+    f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
     Constr_map.iter iter_se db.hintdb_map
 
   let fold f db accu =
@@ -701,7 +728,20 @@ let try_head_pattern c =
 
 let with_uid c = { obj = c; uid = fresh_key () }
 
+let secvars_of_idset s =
+  Id.Set.fold (fun id p ->
+      if is_section_variable id then
+        Id.Pred.add id p
+      else p) s Id.Pred.empty
+
+let secvars_of_constr env c =
+  secvars_of_idset (global_vars_set env c)
+
+let secvars_of_global env gr =
+  secvars_of_idset (vars_of_global_reference env gr)
+
 let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
+  let secvars = secvars_of_constr env c in
   let cty = strip_outer_cast cty in
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
@@ -717,6 +757,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    pat = Some pat;
 	    name = name;
             db = None;
+            secvars;
 	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
@@ -731,6 +772,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
         let nmiss = List.length (clenv_missing ce) in
+        let secvars = secvars_of_constr env c in
 	if Int.equal nmiss 0 then
 	  (Some hd,
           { pri = (match pri with None -> nb_hyp cty | Some p -> p);
@@ -738,6 +780,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
             pat = Some pat;
 	    name = name;
             db = None;
+            secvars;
             code = with_uid (Res_pf(c,cty,ctx)); })
 	else begin
 	  if not eapply then failwith "make_apply_entry";
@@ -750,6 +793,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
              pat = Some pat;
 	     name = name;
              db = None;
+             secvars;
              code = with_uid (ERes_pf(c,cty,ctx)); })
         end
     | _ -> failwith "make_apply_entry"
@@ -806,7 +850,8 @@ let make_resolves env sigma flags pri poly ?name cr =
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
-    [make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name]
+                             [make_exact_entry env sigma pri poly ?name;
+                              make_apply_entry env sigma flags pri poly ?name]
   in
   if List.is_empty ents then
     user_err ~hdr:"Hint"
@@ -818,15 +863,17 @@ let make_resolves env sigma flags pri poly ?name cr =
 (* used to add an hypothesis to the local hint database *)
 let make_resolve_hyp env sigma decl =
   let hname = NamedDecl.get_id decl in
+  let c = mkVar hname in
   try
     [make_apply_entry env sigma (true, true, false) None false
        ~name:(PathHints [VarRef hname])
-       (mkVar hname, NamedDecl.get_type decl, Univ.ContextSet.empty)]
+       (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
 
 (* REM : in most cases hintname = id *)
+
 let make_unfold eref =
   let g = global_of_evaluable_reference eref in
   (Some g,
@@ -835,6 +882,7 @@ let make_unfold eref =
      pat = None;
      name = PathHints [g];
      db = None;
+     secvars = secvars_of_global (Global.env ()) g;
      code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
@@ -845,6 +893,7 @@ let make_extern pri pat tacast =
      pat = pat;
      name = PathAny;
      db = None;
+     secvars = Id.Pred.empty; (* Approximation *)
      code = with_uid (Extern tacast) })  
 
 let make_mode ref m = 
@@ -869,6 +918,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
               pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
 	      name = name;
               db = None;
+              secvars = secvars_of_constr env c;
               code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
 
@@ -1329,7 +1379,7 @@ let pr_hints_db (name,db,hintlist) =
 let pr_hint_list_for_head c =
   let dbs = current_db () in
   let validate (name, db) =
-    let hints = List.map (fun v -> 0, v) (Hint_db.map_all c db) in
+    let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in
     (name, db, hints)
   in
   let valid_dbs = List.map validate dbs in
@@ -1351,9 +1401,9 @@ let pr_hint_term cl =
       let fn = try
 	  let hdc = decompose_app_bound cl in
 	    if occur_existential cl then
-	      Hint_db.map_existential hdc cl
-	    else Hint_db.map_auto hdc cl
-	with Bound -> Hint_db.map_none
+	      Hint_db.map_existential ~secvars:Id.Pred.full hdc cl
+	    else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl
+	with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
       in
       let fn db = List.map (fun x -> 0, x) (fn db) in
       List.map (fun (name, db) -> (name, db, fn db)) dbs
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 48351a317e..edc65c4070 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -28,6 +28,8 @@ val decompose_app_bound : constr -> global_reference * constr array
 
 type debug = Debug | Info | Off
 
+val secvars_of_hyps : Context.Named.t -> Id.Pred.t
+
 (** Pre-created hint databases *)
 
 type 'a hint_ast =
@@ -54,7 +56,8 @@ type 'a with_metadata = private {
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
   name  : hints_path_atom; (** A potential name to refer to the hint *) 
   db    : hint_db_name option;
-  code  : 'a; (** the tactic to apply when the concl matches pat *)
+  secvars : Id.Pred.t; (** The section variables this hint depends on, as a predicate *)
+  code    : 'a; (** the tactic to apply when the concl matches pat *)
 }
 
 type full_hint = hint with_metadata
@@ -85,22 +88,28 @@ module Hint_db :
     type t
     val empty : ?name:hint_db_name -> transparent_state -> bool -> t
     val find : global_reference -> t -> search_entry
-    val map_none : t -> full_hint list
+
+    (** All hints which have no pattern.
+     * [secvars] represent the set of section variables that
+     * can be used in the hint. *)
+    val map_none : secvars:Id.Pred.t -> t -> full_hint list
 
     (** All hints associated to the reference *)
-    val map_all : global_reference -> t -> full_hint list
+    val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments, _not_ using the discrimination net. *)
-    val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list
+    val map_existential : secvars:Id.Pred.t ->
+      (global_reference * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments and using the discrimination net. *)
-    val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list
+    val map_eauto : secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments. *)
-    val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
+    val map_auto : secvars:Id.Pred.t ->
+       (global_reference * constr array) -> constr -> t -> full_hint list
 
     val add_one : env -> evar_map -> hint_entry -> t -> t
     val add_list : env -> evar_map -> hint_entry list -> t -> t
@@ -163,19 +172,20 @@ val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
   env -> evar_map -> open_constr -> hint_term
 
-(** [make_exact_entry pri (c, ctyp)].
+(** [make_exact_entry pri (c, ctyp, ctx, secvars)].
    [c] is the term given as an exact proof to solve the goal;
-   [ctyp] is the type of [c]. *)
-
+   [ctyp] is the type of [c].
+   [ctx] is its (refreshable) universe context. *)
 val make_exact_entry : env -> evar_map -> int option -> polymorphic -> ?name:hints_path_atom -> 
   (constr * types * Univ.universe_context_set) -> hint_entry
 
-(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)].
+(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty,ctx,secvars)].
    [eapply] is true if this hint will be used only with EApply;
    [hnf] should be true if we should expand the head of cty before searching for
    products;
    [c] is the term given as an exact proof to solve the goal;
-   [cty] is the type of [c]. *)
+   [cty] is the type of [c].
+   [ctx] is its (refreshable) universe context. *)
 
 val make_apply_entry :
   env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom -> 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index de328e23f7..e17bbfcb06 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4969,7 +4969,7 @@ module New = struct
   let reduce_after_refine =
     reduce
       (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]})
-      {onhyps=Some []; concl_occs=AllOccurrences }
+      {onhyps=None; concl_occs=AllOccurrences }
 
   let refine ?unsafe c =
     Refine.refine ?unsafe c <*>