Merge PR #11538: Remove many unsafe_type_of uses

Reviewed-by: Matafou
Reviewed-by: gares
Reviewed-by: ppedrot

3 files changed, 37 insertions, 34 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/instances.ml b/plugins/firstorder/instances.ml
index e131cad7da..866b45e4df 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -100,25 +100,28 @@ let rec collect_quantified sigma seq=
 
 let dummy_bvid=Id.of_string "x"
 
-let mk_open_instance env evmap id idc m t =
-  let var_id=
-    if id==dummy_id then dummy_bvid else
-      let typ=Typing.unsafe_type_of env evmap idc in
+let mk_open_instance env sigma id idc m t =
+  let var_id =
+    (* XXX why physical equality? *)
+    if id == dummy_id then dummy_bvid else
+      let typ = Retyping.get_type_of env sigma idc in
         (* since we know we will get a product,
            reduction is not too expensive *)
-      let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
+      let (nam,_,_) = destProd sigma (whd_all env sigma typ) in
         match nam.Context.binder_name with
-            Name id -> id
-          | Anonymous ->  dummy_bvid in
-  let revt=substl (List.init m (fun i->mkRel (m-i))) t in
-  let rec aux n avoid env evmap decls =
-    if Int.equal n 0 then evmap, decls else
-      let nid=(fresh_id_in_env avoid var_id env) in
-      let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+        | Name id -> id
+        | Anonymous ->  dummy_bvid
+  in
+  let revt = substl (List.init m (fun i->mkRel (m-i))) t in
+  let rec aux n avoid env sigma decls =
+    if Int.equal n 0 then sigma, decls else
+      let nid = fresh_id_in_env avoid var_id env in
+      let (sigma, (c, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in
       let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in
-        aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
-  let evmap, decls = aux m Id.Set.empty env evmap [] in
-  (evmap, decls, revt)
+      aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) sigma (decl::decls)
+  in
+  let sigma, decls = aux m Id.Set.empty env sigma [] in
+  (sigma, decls, revt)
 
 (* tactics   *)
 
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=