Remove unsafe_type_of from funind

7 files changed, 54 insertions, 49 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ad1c70b7bf..9749af1e66 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -536,22 +536,23 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
                            );
                    anomaly (Pp.str "cannot compute new term value.")
            in
-         let fun_body =
-           mkLambda(make_annot Anonymous Sorts.Relevant,
-                    pf_unsafe_type_of g' term,
-                    Termops.replace_term (project g') term (mkRel 1) dyn_infos.info
-                   )
-         in
-         let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
-         let new_infos =
-           {dyn_infos with
+           let g', termtyp = tac_type_of g' term in
+           let fun_body =
+             mkLambda(make_annot Anonymous Sorts.Relevant,
+                      termtyp,
+                      Termops.replace_term (project g') term (mkRel 1) dyn_infos.info
+                     )
+           in
+           let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
+           let new_infos =
+             {dyn_infos with
               info = new_body;
               eq_hyps = heq_id::dyn_infos.eq_hyps
-           }
-         in
-         clean_goal_with_heq ptes_infos continue_tac new_infos  g'
-      )])
-    ]
+             }
+           in
+           clean_goal_with_heq ptes_infos continue_tac new_infos  g'
+          )])
+      ]
       g
 
 
@@ -633,7 +634,7 @@ let build_proof
                   let dyn_infos = {dyn_info' with info =
                       mkCase(ci,ct,t,cb)} in
                   let g_nb_prod = nb_prod (project g) (pf_concl g) in
-                  let type_of_term = pf_unsafe_type_of g t in
+                  let g, type_of_term = tac_type_of g t in
                   let term_eq =
                     make_refl_eq (Lazy.force refl_equal) type_of_term t
                   in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 8def5c60ba..68661174ac 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -993,7 +993,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
     let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i))  in
-    let princ_type = pf_unsafe_type_of g graph_principle in
+    let g, princ_type = tac_type_of g graph_principle in
     let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
@@ -1210,7 +1210,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
   in
   let _ = evd := sigma in
   let l_schemes =
-    List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
+    List.map (EConstr.of_constr %> Retyping.get_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
   in
   let i = ref (-1) in
   let sorts =
@@ -2051,7 +2051,7 @@ let build_case_scheme fa =
   let (sigma, scheme) =
       Indrec.build_case_analysis_scheme_default env sigma ind sf
   in
-  let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
+  let scheme_type = EConstr.Unsafe.to_constr ((Retyping.get_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
        fst @@ UnivGen.fresh_sort_in_family x
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index bf32f7af19..84f09c385f 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -514,8 +514,9 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
                    a pseudo value "v1 ... vn".
                    The "value" of this branch is then simply [res]
                 *)
+                (* XXX here and other [understand] calls drop the ctx *)
                 let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
-                let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
+                let rt_typ = Retyping.get_type_of env (Evd.from_env env) rt_as_constr in
                 let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
                 let res = fresh_id args_res.to_avoid "_res" in
                 let new_avoid = res::args_res.to_avoid in
@@ -629,7 +630,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
         let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
         let v_res = build_entry_lc env sigma funnames avoid v in
         let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
-        let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
+        let v_type = Retyping.get_type_of env (Evd.from_env env) v_as_constr in
         let v_r = Sorts.Relevant in (* TODO relevance *)
         let new_env =
           match n with
@@ -646,7 +647,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
         build_entry_lc_from_case env sigma funnames make_discr el brl avoid
     | GIf(b,(na,e_option),lhs,rhs) ->
         let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-        let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+        let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
         let (ind,_) =
           try Inductiveops.find_inductive env (Evd.from_env env) b_typ
           with Not_found ->
@@ -678,7 +679,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
               nal
           in
           let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-          let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+          let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
           let (ind,_) =
             try Inductiveops.find_inductive env (Evd.from_env env) b_typ
             with Not_found ->
@@ -723,7 +724,7 @@ and build_entry_lc_from_case env sigma funname make_discr
         let types =
           List.map (fun (case_arg,_) ->
                       let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
-                      EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr)
+                      EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) case_arg_as_constr)
                    ) el
         in
         (****** The next works only if the match is not dependent ****)
@@ -1164,7 +1165,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
           let evd = (Evd.from_env env) in
           let t',ctx = Pretyping.understand env evd t in
           let evd = Evd.from_ctx ctx in
-          let type_t' = Typing.unsafe_type_of env evd t' in
+          let type_t' = Retyping.get_type_of env evd t' in
           let t' = EConstr.Unsafe.to_constr t' in
           let type_t' = EConstr.Unsafe.to_constr type_t' in
           let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a205c0744a..f28e98dcc2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -64,12 +64,10 @@ let functional_induction with_clean c princl pat =
             | InSet -> finfo.rec_lemma
             | InType -> finfo.rect_lemma
           in
-          let princ =  (* then we get the principle *)
+          let sigma, princ =  (* then we get the principle *)
             match princ_option with
             | Some princ ->
-              let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) in
-              Proofview.Unsafe.tclEVARS sigma >>= fun () ->
-              Proofview.tclUNIT princ
+              Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ)
             | None ->
               (*i If there is not default lemma defined then,
                       we cross our finger and try to find a lemma named f_ind
@@ -87,19 +85,18 @@ let functional_induction with_clean c princl pat =
                   user_err (str "Cannot find induction principle for "
                             ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
               in
-              let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) princ_ref in
-              Proofview.Unsafe.tclEVARS sigma >>= fun () ->
-              Proofview.tclUNIT princ
+              Evd.fresh_global (pf_env gl) (project gl) princ_ref
           in
-          princ >>= fun princ ->
-          (* We need to refresh gl due to the updated evar_map in princ *)
-          Proofview.Goal.enter_one (fun gl ->
-          Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args))
+          let princt = Retyping.get_type_of (pf_env gl) sigma princ in
+          Proofview.Unsafe.tclEVARS sigma <*>
+          Proofview.tclUNIT (princ, Tactypes.NoBindings, princt, args)
         | _ ->
           CErrors.user_err (str "functional induction must be used with a function" )
       end
     | Some ((princ,binding)) ->
-      Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args)
+      let sigma, princt = pf_type_of gl princ in
+      Proofview.Unsafe.tclEVARS sigma <*>
+      Proofview.tclUNIT (princ, binding, princt, args)
     ) >>= fun (princ, bindings, princ_type, args) ->
   Proofview.Goal.enter (fun gl ->
   let sigma = project gl in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b55d8537d6..bce09d8fbd 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -526,3 +526,7 @@ let funind_purify f x =
     let e = CErrors.push e in
     Vernacstate.unfreeze_interp_state st;
     Exninfo.iraise e
+
+let tac_type_of g c =
+  let sigma, t = Tacmach.pf_type_of g c in
+  {g with Evd.sigma}, t
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 550f727951..bd8b34088b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -119,3 +119,5 @@ type tcc_lemma_value =
   | Not_needed
 
 val funind_purify : ('a -> 'b) -> ('a -> 'b)
+
+val tac_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Goal.goal Evd.sigma * EConstr.types
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 93ed1510d0..f7f8004998 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -31,7 +31,6 @@ open Tactics
 open Nametab
 open Declare
 open Tacred
-open Goal
 open Glob_term
 open Pretyping
 open Termops
@@ -110,9 +109,10 @@ let pf_get_new_ids idl g =
 let next_ident_away_in_goal ids avoid =
   next_ident_away_in_goal ids (Id.Set.of_list avoid)
 
-let compute_renamed_type gls c =
+let compute_renamed_type gls id =
   rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) []
-    (pf_unsafe_type_of gls c)
+    (pf_get_hyp_typ gls id)
+
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"
@@ -645,9 +645,7 @@ let pf_typel l tac =
   modified hypotheses are generalized in the process and should be
   introduced back later; the result is the pair of the tactic and the
   list of hypotheses that have been generalized and cleared. *)
-let mkDestructEq :
-  Id.t list -> constr -> goal Evd.sigma -> tactic * Id.t list =
-  fun not_on_hyp expr g ->
+let mkDestructEq not_on_hyp expr g =
   let hyps = pf_hyps g in
   let to_revert =
     Util.List.map_filter
@@ -657,9 +655,9 @@ let mkDestructEq :
         if Id.List.mem id not_on_hyp || not (Termops.dependent (project g) expr (get_type decl))
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
-  let type_of_expr = pf_unsafe_type_of g expr in
-  let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
-           to_revert_constr in
+  let g, type_of_expr = tac_type_of g expr in
+  let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::to_revert_constr in
+  let tac =
     pf_typel new_hyps (fun _ ->
     observe_tclTHENLIST (fun _ _ -> str "mkDestructEq")
      [Proofview.V82.of_tactic (generalize new_hyps);
@@ -668,7 +666,9 @@ let mkDestructEq :
           pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
         in
         Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2);
-      Proofview.V82.of_tactic (simplest_case expr)]), to_revert
+      Proofview.V82.of_tactic (simplest_case expr)])
+  in
+  g, tac, to_revert
 
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
   let sigma = project g in
@@ -686,7 +686,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
       info = mkCase(ci,t,a',l);
       is_main_branch = expr_info.is_main_branch;
       is_final = expr_info.is_final} in
-  let destruct_tac,rev_to_thin_intro =
+  let g,destruct_tac,rev_to_thin_intro =
     mkDestructEq [expr_info.rec_arg_id] a' g in
   let to_thin_intro = List.rev rev_to_thin_intro in
   observe_tac (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a')
@@ -842,7 +842,7 @@ let rec make_rewrite_list expr_info max = function
       (observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p ) (
         (fun g ->
           let sigma = project g in
-          let t_eq = compute_renamed_type g (mkVar hp) in
+          let t_eq = compute_renamed_type g hp in
           let k,def =
             let k_na,_,t = destProd sigma t_eq in
             let _,_,t  = destProd sigma t in
@@ -868,7 +868,7 @@ let make_rewrite expr_info l hp max =
     (observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS
        (fun g ->
           let sigma = project g in
-          let t_eq = compute_renamed_type g (mkVar hp) in
+          let t_eq = compute_renamed_type g hp in
           let k,def =
             let k_na,_,t = destProd sigma t_eq in
             let _,_,t  = destProd sigma t in