various unsafe_type_of -> type_of_variable in funind

This is the easy part of removing unsafe_type_of, as type_of_variable
doesn't return (or even take as argument) an evar map.

5 files changed, 14 insertions, 16 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 00f4be783d..ad1c70b7bf 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -475,7 +475,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
       tclIDTAC
   in
   try
-    scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
+    scan_type [] (Typing.type_of_variable env hyp_id), [hyp_id]
   with TOREMOVE ->
     thin [hyp_id],[]
 
@@ -525,7 +525,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
         tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps;
         observe_tac "after_introduction" (fun g' ->
            (* We get infos on the equations introduced*)
-           let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
+           let new_term_value_eq = pf_get_hyp_typ g' heq_id in
            (* compute the new value of the body *)
            let new_term_value =
              match EConstr.kind (project g') new_term_value_eq with
@@ -849,7 +849,7 @@ let generalize_non_dep hyp g =
 (*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
   let hyps = [hyp] in
   let env = Global.env () in
-  let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
+  let hyp_typ = pf_get_hyp_typ g hyp in
   let to_revert,_ =
     let open Context.Named.Declaration in
     Environ.fold_named_context_reverse (fun (clear,keep) decl ->
@@ -1351,7 +1351,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
     let rewrite =
       tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
     in
-    let _,hrec_concl  = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) in
+    let _,hrec_concl  = decompose_prod (project gls) (pf_get_hyp_typ gls hrec) in
     let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in
     let f =  (fst (destApp (project gls) f_app)) in
     let rec backtrack : tactic =
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 58efee1518..8def5c60ba 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -617,7 +617,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       let constructor_args g =
         List.fold_right
           (fun hid acc ->
-             let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
+             let type_of_hid = pf_get_hyp_typ g hid in
              let sigma = project g in
              match EConstr.kind sigma type_of_hid with
              | Prod(_,_,t') ->
@@ -953,7 +953,7 @@ let rec reflexivity_with_destruct_cases g =
         match sc with
           None -> tclIDTAC g
         | Some id ->
-          match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with
+          match EConstr.kind (project g) (pf_get_hyp_typ g id) with
           | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
             if Equality.discriminable (pf_env g) (project g) t1 t2
             then Proofview.V82.of_tactic (Equality.discrHyp id) g
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e41b92d4dc..bf32f7af19 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -769,9 +769,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to
                  let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
                    List.fold_right
                      (fun id acc ->
-                        let typ_of_id =
-                          Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
-                        in
+                        let typ_of_id = Typing.type_of_variable env_with_pat_ids id in
                         let raw_typ_of_id =
                           Detyping.detype Detyping.Now false Id.Set.empty
                             env_with_pat_ids (Evd.from_env env) typ_of_id
@@ -832,7 +830,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to
                    (fun id  acc ->
                       if Id.Set.mem id this_pat_ids
                       then (Prod (Name id),
-                      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
+                      let typ_of_id = Typing.type_of_variable new_env id in
                       let raw_typ_of_id =
                         Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
                       in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d72319d078..332d058ce7 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -28,7 +28,7 @@ open Indfun_common
 *)
 let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
   let sigma = project gl in
-  let typ = pf_unsafe_type_of gl (mkVar hid) in
+  let typ = pf_get_hyp_typ hid gl in
   match EConstr.kind sigma typ with
   | App(i,args) when isInd sigma i ->
     let ((kn',num) as ind'),u = destInd sigma i in
@@ -77,7 +77,7 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
 let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl ->
   let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps gl) Id.Set.empty in
   let sigma = project gl in
-  let type_of_h = pf_unsafe_type_of gl (mkVar hid) in
+  let type_of_h = pf_get_hyp_typ hid gl in
   match EConstr.kind sigma type_of_h with
   | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
     let pre_tac,f_args,res =
@@ -128,7 +128,7 @@ let invfun qhyp f =
   | None ->
     let tac_action hid gl =
       let sigma = project gl in
-      let hyp_typ = pf_unsafe_type_of gl (mkVar hid)  in
+      let hyp_typ = pf_get_hyp_typ hid gl  in
       match EConstr.kind sigma hyp_typ with
       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
         begin
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 66ed1961ba..93ed1510d0 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -370,7 +370,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
             Proofview.V82.of_tactic (clear to_intros);
             h_intros to_intros;
             (fun g' ->
-              let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
+              let ty_teq = pf_get_hyp_typ g' heq in
               let teq_lhs,teq_rhs =
                 let _,args = try destApp (project g') ty_teq with DestKO -> assert false in
                 args.(1),args.(2)
@@ -487,13 +487,13 @@ let rec prove_lt hyple g =
       in
       let h =
         List.find (fun id ->
-          match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with
+          match decompose_app sigma (pf_get_hyp_typ g id) with
             | _, t::_ -> EConstr.eq_constr sigma t varx
             | _ -> false
         ) hyple
       in
       let y =
-        List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in
+        List.hd (List.tl (snd (decompose_app sigma (pf_get_hyp_typ g h)))) in
       observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[
         Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
         observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple)