Fix bug #4354: interpret hints in the right env and sigma.

5 files changed, 25 insertions, 20 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 72ba9e0bd9..e5fdf6a7c2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -309,7 +309,8 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
           let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
           let hyp = Context.map_named_declaration nf decl in
 	  let hintl = make_resolve_hyp env sigma hyp
-	  in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)
+	  in trivial_fail_db dbg mod_delta db_list
+	       (Hint_db.add_list env sigma hintl local_db)
       end)
   in
   Proofview.Goal.enter begin fun gl ->
@@ -438,7 +439,9 @@ let possible_resolve dbg mod_delta db_list local_db cl =
   with Not_found -> []
 
 let extend_local_db decl db gl =
-  Hint_db.add_list (make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) decl) db
+  let env = Tacmach.New.pf_env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db
 
 (* Introduce an hypothesis, then call the continuation tactic [kont]
    with the hint db extended with the so-obtained hypothesis *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 80f47c680f..ed5b783f6c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -190,7 +190,7 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
-	      (Hint_db.add_list hintl local_db) g'))) ::
+	      (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) ::
     (List.map (fun (x,_,_,_,_) -> x) 
      (e_trivial_resolve db_list local_db (project goal) (pf_concl goal)))
   in
@@ -339,7 +339,7 @@ let make_hints g st only_classes sign =
 	  (PathOr (paths, path), hint @ hints)
       else (paths, hints))
     (PathEmpty, []) sign
-  in Hint_db.add_list hintlist (Hint_db.empty st true)
+  in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true)
 
 let make_autogoal_hints =
   let cache = ref (true, Environ.empty_named_context_val, 
@@ -374,7 +374,7 @@ let intro_tac : atac =
 	  let context = Environ.named_context_of_val (Goal.V82.hyps s g') in
 	  let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
 	    (true,false,false) info.only_classes None (List.hd context) in
-	  let ldb = Hint_db.add_list hint info.hints in
+	  let ldb = Hint_db.add_list env s hint info.hints in
 	    (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls
       in {it = gls'; sigma = s;})
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 34f87c6cf0..83498cabd8 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -147,7 +147,7 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
-	      (Hint_db.add_list hintl local_db) g'))) ::
+	      (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) ::
     (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in
     tclFIRST (List.map tclCOMPLETE tacl) goal
@@ -269,7 +269,8 @@ module SearchProblem = struct
 	     let hintl =
 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 	     in
-             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
+             let ldb = Hint_db.add_list (pf_env g') (project g')
+		  hintl (List.hd s.localdb) in
 	     { depth = s.depth; priority = cost; tacres = lgls;
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb; prev = ps })
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a7eae667d0..dbb2340364 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -266,11 +266,10 @@ let strip_params env c =
     | _ -> c)
   | _ -> c
 
-let instantiate_hint p =
+let instantiate_hint env sigma p =
   let mk_clenv c cty ctx =
-    let env = Global.env () in
-    let sigma = Evd.merge_context_set univ_flexible (Evd.from_env env) ctx in
-    let cl = mk_clenv_from_env (Global.env()) sigma None (c,cty) in 
+    let sigma = Evd.merge_context_set univ_flexible sigma ctx in
+    let cl = mk_clenv_from_env env sigma None (c,cty) in 
       {cl with templval = 
 	  { cl.templval with rebus = strip_params env cl.templval.rebus };
 	env = empty_env}
@@ -524,8 +523,8 @@ module Hint_db = struct
     in
       List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat
 
-  let add_one (k, v) db =
-    let v = instantiate_hint v in
+  let add_one env sigma (k, v) db =
+    let v = instantiate_hint env sigma v in
     let st',db,rebuild =
       match v.code.obj with
       | Unfold_nth egr ->
@@ -542,7 +541,7 @@ module Hint_db = struct
     let db, id = next_hint_id db in
     addkv k id v db
 
-  let add_list l db = List.fold_left (fun db k -> add_one k db) db l
+  let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l
 
   let remove_sdl p sdl = List.smartfilter p sdl 
 
@@ -812,7 +811,9 @@ let add_hint dbname hintlist =
   in
   let () = List.iter check hintlist in
   let db = get_db dbname in
-  let db' = Hint_db.add_list hintlist db in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let db' = Hint_db.add_list env sigma hintlist db in
     searchtable_add (dbname,db')
 
 let add_transparency dbname grs b =
@@ -1166,8 +1167,8 @@ let expand_constructor_hints env sigma lems =
 let add_hint_lemmas env sigma eapply lems hint_db =
   let lems = expand_constructor_hints env sigma lems in
   let hintlist' =
-    List.map_append (make_resolves env sigma (eapply,true,false) None true) lems in
-  Hint_db.add_list hintlist' hint_db
+    List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in
+  Hint_db.add_list env sigma hintlist' hint_db
 
 let make_local_hint_db env sigma ts eapply lems =
   let sign = Environ.named_context env in
@@ -1177,7 +1178,7 @@ let make_local_hint_db env sigma ts eapply lems =
   in
   let hintlist = List.map_append (make_resolve_hyp env sigma) sign in
   add_hint_lemmas env sigma eapply lems
-    (Hint_db.add_list hintlist (Hint_db.empty ts false))
+    (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false))
 
 let make_local_hint_db = 
   if Flags.profile then
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 687bc78c76..5a4fb77091 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -93,8 +93,8 @@ module Hint_db :
 	arguments. *)
     val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
 
-    val add_one : hint_entry -> t -> t
-    val add_list : (hint_entry) list -> t -> t
+    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
     val remove_list : global_reference list -> t -> t
     val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit