From 0aec9033a0b78ee1629f7aabce1c8a2e3cfbe619 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 12 Oct 2016 16:18:02 +0200
Subject: 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.
---
 tactics/auto.ml          |  41 ++++++++++-------
 tactics/auto.mli         |   2 +
 tactics/class_tactics.ml |  40 +++++++++--------
 tactics/eauto.ml         |  32 +++++++------
 tactics/hints.ml         | 115 +++++++++++++++++++++++++++++++++--------------
 tactics/hints.mli        |  32 ++++++++-----
 6 files changed, 169 insertions(+), 93 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0f5b74d9da..9ab53b75d9 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 5384140c2a..ccfb520f1d 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 0944cbe38f..9cb6b7fe78 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 c6d2448679..fbaefaf43c 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 89ecc6c0b2..823af0b0a5 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 411540aa1b..8145ae1936 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 -> 
-- 
cgit v1.2.3


From 9194180e2da0f7f9a2b2c7574bb7261cc69ead17 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 25 Oct 2016 14:02:49 +0200
Subject: Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4
 behavior)."

This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6.

This behavior of refine has changed three times in recent years, so
let's take the time to make up our mind and wait for a major release.
Btw, onhyps=None is not a sane way to express that a tactic should be
applied to all hypotheses.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 225ff3db94..549799974b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4589,7 +4589,7 @@ module New = struct
   let reduce_after_refine =
     Proofview.V82.tactic (reduce
       (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
-      {onhyps=Some []; concl_occs=AllOccurrences })
+      {onhyps=None; concl_occs=AllOccurrences })
 
   let refine ?unsafe c =
     Proofview.Refine.refine ?unsafe c <*>
-- 
cgit v1.2.3


From d2e713c3913c995ba3796863f778556e00cc5051 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 19 Oct 2016 18:30:44 +0200
Subject: Remove warning now that info_auto is fixed.

Removes a warning dating from 8.5 signaling that info_auto
and info_trivial are broken and advising to use Info 1 auto
instead. Now, these tactics are fixed and thus they can be
used again. They do not do exactly the same thing as
Info 1 auto and may be more useful for the learner.
---
 tactics/tacinterp.ml | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c3f7fa1439..23d188aa73 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2023,12 +2023,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
-      begin if debug == Tacexpr.Info then
-          msg_warning
-	    (strbrk"The \"info_trivial\" tactic" ++ spc ()
-           ++strbrk"does not print traces anymore." ++ spc()
-           ++strbrk"Use \"Info 1 trivial\", instead.")
-      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
@@ -2039,13 +2033,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	     lems
 	     (Option.map (List.map (interp_hint_base ist)) l))
       end
+
   | TacAuto (debug,n,lems,l) ->
-      begin if debug == Tacexpr.Info then
-          msg_warning
-	    (strbrk"The \"info_auto\" tactic" ++ spc ()
-           ++strbrk"does not print traces anymore." ++ spc()
-           ++strbrk"Use \"Info 1 auto\", instead.")
-      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-- 
cgit v1.2.3


From d500a684be14b0c781ea4cda0ee02d3c5cdcad81 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Oct 2016 19:33:56 +0200
Subject: Using msg_info for info_auto and info_eauto (PR #324).

---
 tactics/auto.ml  | 8 ++++----
 tactics/eauto.ml | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0f5b74d9da..6c5ecac943 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -260,19 +260,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
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index c6d2448679..5ca68cbe96 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -346,13 +346,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 +363,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)
-- 
cgit v1.2.3