Merge PR #11538: Remove many unsafe_type_of uses

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

2 files changed, 33 insertions, 31 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 500f464ea7..fdc70ccaa8 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -492,7 +492,7 @@ let rec add_term state t=
         Not_found ->
           let b=next uf in
           let trm = constr_of_term t in
-          let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in
+          let typ = Retyping.get_type_of state.env state.sigma (EConstr.of_constr trm) in
           let typ = canonize_name state.sigma typ in
           let new_node=
             match t with
@@ -809,23 +809,23 @@ let new_state_var typ state =
 
 let complete_one_class state i=
   match (get_representative state.uf i).inductive_status with
-      Partial pac ->
-        let rec app t typ n =
-          if n<=0 then t else
-            let _,etyp,rest= destProd typ in
-            let id = new_state_var (EConstr.of_constr etyp) state in
-                app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
-        let _c = Typing.unsafe_type_of state.env state.sigma
-          (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
-        let _c = EConstr.Unsafe.to_constr _c in
-        let _args =
-          List.map (fun i -> constr_of_term (term state.uf  i))
-            pac.args in
-        let typ = Term.prod_applist _c (List.rev _args) in
-        let ct = app (term state.uf i) typ pac.arity in
-          state.uf.epsilons <- pac :: state.uf.epsilons;
-          ignore (add_term state ct)
-    | _ -> anomaly (Pp.str "wrong incomplete class.")
+  | Partial pac ->
+    let rec app t typ n =
+      if n<=0 then t else
+        let _,etyp,rest= destProd typ in
+        let id = new_state_var (EConstr.of_constr etyp) state in
+        app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
+    let c = Retyping.get_type_of state.env state.sigma
+        (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
+    let c = EConstr.Unsafe.to_constr c in
+    let args =
+      List.map (fun i -> constr_of_term (term state.uf  i))
+        pac.args in
+    let typ = Term.prod_applist c (List.rev args) in
+    let ct = app (term state.uf i) typ pac.arity in
+    state.uf.epsilons <- pac :: state.uf.epsilons;
+    ignore (add_term state ct)
+  | _ -> anomaly (Pp.str "wrong incomplete class.")
 
 let complete state =
   Int.Set.iter (complete_one_class state) state.pa_classes
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 556e6b48e6..8a650d9e7a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -277,10 +277,12 @@ let refresh_type env evm ty =
   Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
                               (Some false) env evm ty
 
-let refresh_universes ty k =
+let type_and_refresh c k =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
+    (* XXX is get_type_of enough? *)
+    let evm, ty = Typing.type_of env evm c in
     let evm, ty = refresh_type env evm ty in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty)
   end
@@ -289,7 +291,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.enter begin fun gl ->
-  let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check (EConstr.of_constr c)
@@ -297,17 +298,17 @@ let rec proof_tac p : unit Proofview.tactic =
         let c = EConstr.of_constr c in
         let l=constr_of_term p.p_lhs and
             r=constr_of_term p.p_rhs in
-        refresh_universes (type_of l) (fun typ ->
+        type_and_refresh l (fun typ ->
         app_global _sym_eq [|typ;r;l;c|] exact_check)
     | Refl t ->
         let lr = constr_of_term t in
-        refresh_universes (type_of lr) (fun typ ->
+        type_and_refresh lr (fun typ ->
         app_global _refl_equal [|typ;constr_of_term t|] exact_check)
     | Trans (p1,p2)->
         let t1 = constr_of_term p1.p_lhs and
             t2 = constr_of_term p1.p_rhs and
             t3 = constr_of_term p2.p_rhs in
-        refresh_universes (type_of t2) (fun typ ->
+        type_and_refresh t2 (fun typ ->
         let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
           Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)])
     | Congr (p1,p2)->
@@ -315,9 +316,9 @@ let rec proof_tac p : unit Proofview.tactic =
         and tx1=constr_of_term p2.p_lhs
         and tf2=constr_of_term p1.p_rhs
         and tx2=constr_of_term p2.p_rhs in
-        refresh_universes (type_of tf1) (fun typf ->
-        refresh_universes (type_of tx1) (fun typx ->
-        refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
+        type_and_refresh tf1 (fun typf ->
+        type_and_refresh tx1 (fun typx ->
+        type_and_refresh (mkApp (tf1,[|tx1|])) (fun typfx ->
         let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
         let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in
         let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
@@ -341,8 +342,8 @@ let rec proof_tac p : unit Proofview.tactic =
          let tj=constr_of_term prf.p_rhs in
          let default=constr_of_term p.p_lhs in
          let special=mkRel (1+nargs-argind) in
-         refresh_universes (type_of ti) (fun intype ->
-         refresh_universes (type_of default) (fun outtype ->
+         type_and_refresh ti (fun intype ->
+         type_and_refresh default (fun outtype ->
          let sigma, proj =
            build_projection intype cstr special default gl
          in
@@ -362,7 +363,7 @@ let refute_tac c t1 t2 p =
     let neweq= app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
+  in type_and_refresh tt1 k
   end
 
 let refine_exact_check c =
@@ -382,7 +383,7 @@ let convert_to_goal_tac c t1 t2 p =
     let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
                            [proof_tac p; endt refine_exact_check]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
+  in type_and_refresh tt2 k
   end
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -401,7 +402,8 @@ let discriminate_tac cstru p =
     let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in
+    let evm, intype = Typing.type_of env evm lhs in
+    let evm, intype = refresh_type env evm intype in
     let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
     let neweq=app_global _eq [|intype;lhs;rhs|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)