unsafe_type_of -> type_of in Sequent.extend_with_auto_hints

+ fix evar leak in caller

3 files changed, 21 insertions, 19 deletions

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 8946587a02..9d208e1c86 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -88,7 +88,7 @@ let gen_ground_tac flag taco ids bases =
         Proofview.Goal.enter begin fun gl ->
         let seq=empty_seq !ground_depth in
         let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
-        let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
+        let seq, sigma = extend_with_auto_hints (pf_env gl) sigma bases seq in
         tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
         end
       in
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7d84ee6851..65af123d9c 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -204,28 +204,28 @@ let extend_with_ref_list env sigma l seq =
 open Hints
 
 let extend_with_auto_hints env sigma l seq =
-  let seqref=ref seq in
-  let f p_a_t =
+  let f (seq,sigma) p_a_t =
     match repr_hint p_a_t.code with
-        Res_pf (c,_) | Give_exact (c,_)
-      | Res_pf_THEN_trivial_fail (c,_) ->
-          let (c, _, _) = c in
-          (try
-             let (gr, _) = Termops.global_of_constr sigma c in
-             let typ=(Typing.unsafe_type_of env sigma c) in
-               seqref:=add_formula env sigma Hint gr typ !seqref
-           with Not_found->())
-      | _-> () in
-  let g _ _ l = List.iter f l in
-  let h dbname=
-    let hdb=
+    | Res_pf (c,_) | Give_exact (c,_)
+    | Res_pf_THEN_trivial_fail (c,_) ->
+      let (c, _, _) = c in
+      (try
+         let (gr, _) = Termops.global_of_constr sigma c in
+         let sigma, typ = Typing.type_of env sigma c in
+         add_formula env sigma Hint gr typ seq, sigma
+       with Not_found -> seq, sigma)
+    | _ -> seq, sigma
+  in
+  let h acc dbname =
+    let hdb =
       try
         searchtable_map dbname
       with Not_found->
-        user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in
-      Hint_db.iter g hdb in
-    List.iter h l;
-    !seqref, sigma (*FIXME: forgetting about universes*)
+        user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database"))
+    in
+    Hint_db.fold (fun _ _ l acc -> List.fold_left f acc l) hdb acc
+  in
+  List.fold_left h (seq,sigma) l
 
 let print_cmap map=
   let print_entry c l s=
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 2a9b71387e..9c9f0b7708 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -160,6 +160,8 @@ module Hint_db :
     val iter : (GlobRef.t option ->
                 hint_mode array list -> full_hint list -> unit) -> t -> unit
 
+    val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a
+
     val use_dn : t -> bool
     val transparent_state : t -> TransparentState.t
     val set_transparent_state : t -> TransparentState.t -> t