Tacmach API using EConstr.

2 files changed, 8 insertions, 7 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc53b113d..102efe55b 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -508,7 +508,7 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
           let trm = constr_of_term t in
-	  let typ = pf_unsafe_type_of state.gls trm in
+	  let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
 	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
@@ -832,7 +832,7 @@ let complete_one_class state i=
 	    let id = new_state_var etyp state in
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
 	let _c = pf_unsafe_type_of state.gls
-	  (constr_of_term (term state.uf pac.cnode)) in
+	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 11da923e1..7c78f3a17 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -243,7 +243,8 @@ let app_global f args k =
 let new_app_global f args k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
-let new_refine c = Proofview.V82.tactic (refine c)
+let new_refine c = Proofview.V82.tactic (refine (EConstr.of_constr c))
+let refine c = refine (EConstr.of_constr c)
 
 let assert_before n c =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -265,7 +266,7 @@ let refresh_universes ty k =
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
+  let type_of t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t) in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check c
@@ -336,7 +337,7 @@ let refute_tac c t1 t2 p =
     let neweq= new_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 refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt1)) k
   end }
 
 let refine_exact_check c gl =
@@ -354,7 +355,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; Proofview.V82.tactic (endt refine_exact_check)]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt2)) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -376,7 +377,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let identity = Universes.constr_of_global (Lazy.force _I) in
     let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
+    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1))) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in