sections/hints: prevent Not_found in get_type_of

due to cleared/reverted section variables.
This fixes the get_type_of but requires keeping information
around about the section hyps available in goals during resolution.
It's optimized for the non-section case (should incur no cost there),
and the case where no section variables are cleared.

9 files changed, 192 insertions, 93 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 17e56ec31..35cacc65b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -599,6 +599,10 @@ let collect_vars c =
   | _ -> fold_constr aux vars c in
   aux Id.Set.empty c
 
+let vars_of_global_reference env gr =
+  let c, _ = Universes.unsafe_constr_of_global gr in
+  vars_of_global (Global.env ()) c
+
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 0a7ac1f26..fd8edafbc 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -121,6 +121,7 @@ val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool
 val count_occurrences : constr -> constr -> int
 val collect_metas : constr -> int list
 val collect_vars : constr -> Id.Set.t (** for visible vars only *)
+val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t
 val occur_term : constr -> constr -> bool (** Synonymous
  of dependent 
    Substitution of metavariables *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0f5b74d9d..9ab53b75d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -35,6 +35,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) *)
 
@@ -295,12 +299,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
@@ -325,22 +330,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 ->
@@ -360,11 +366,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)
@@ -397,7 +403,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
@@ -406,7 +412,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
@@ -444,7 +450,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
@@ -452,7 +458,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 =
@@ -483,11 +489,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 5384140c2..ccfb520f1 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -15,6 +15,8 @@ open Pattern
 open Decl_kinds
 open Hints
 
+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 0944cbe38..9cb6b7fe7 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -280,11 +280,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
@@ -339,7 +339,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 =
@@ -350,13 +350,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}
@@ -367,7 +367,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
@@ -384,15 +384,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
@@ -429,7 +429,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
@@ -449,15 +449,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 c6d244867..fbaefaf43 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) ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 89ecc6c0b..823af0b0a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -66,6 +66,24 @@ 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 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                 *)
 (************************************************************************)
@@ -104,12 +122,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
@@ -418,11 +437,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
@@ -471,7 +493,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
@@ -489,40 +515,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
@@ -598,11 +624,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 =
@@ -698,7 +724,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"
@@ -714,6 +753,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) =
@@ -728,6 +768,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);
@@ -735,6 +776,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";
@@ -747,6 +789,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"
@@ -803,7 +846,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
     errorlabstrm "Hint"
@@ -815,15 +859,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 = 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, get_type decl, Univ.ContextSet.empty)]
+       (c, 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,
@@ -832,6 +878,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 =
@@ -843,6 +890,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 = 
@@ -867,6 +915,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)) })
 
 
@@ -1327,7 +1376,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
@@ -1349,9 +1398,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 411540aa1..8145ae193 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -25,6 +25,8 @@ exception Bound
 
 val decompose_app_bound : constr -> global_reference * constr array
 
+val secvars_of_hyps : Context.Named.t -> Id.Pred.t
+
 (** Pre-created hint databases *)
 
 type 'a hint_ast =
@@ -51,7 +53,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
@@ -82,22 +85,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
@@ -160,19 +169,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/test-suite/success/clear.v b/test-suite/success/clear.v
index 976bec737..e25510cf0 100644
--- a/test-suite/success/clear.v
+++ b/test-suite/success/clear.v
@@ -13,3 +13,21 @@ Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True.
   reflexivity.
 Qed.
 
+Class A.
+
+Section Foo.
+
+  Variable a : A.
+
+  Goal A.
+    solve [typeclasses eauto].
+    Undo 1.
+    clear a.
+    try typeclasses eauto.
+    assert(a:=Build_A).
+    solve [ typeclasses eauto ].
+    Undo 2.
+    assert(b:=Build_A).
+    solve [ typeclasses eauto ].
+  Qed.
+End Foo.
\ No newline at end of file