unsafe_type_of -> type_of in Cctac (with small refactor)

Not sure if get_type_of would be fine, let's go with this for now.

1 files changed, 15 insertions, 13 deletions

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)