Removing various compatibility layers of tactics.

2 files changed, 10 insertions, 8 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 0a980c03b..aedcb7575 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -452,8 +452,9 @@ and applist_projection c l =
       applistc (mkProj (p, hd)) tl)
   | _ -> applistc c l
 
-let rec canonize_name c =
-  let func =  canonize_name in
+let rec canonize_name sigma c =
+  let c = EConstr.Unsafe.to_constr c in
+  let func c = canonize_name sigma (EConstr.of_constr c) in
     match kind_of_term c with
       | Const (kn,u) ->
 	  let canon_const = constant_of_kn (canonical_con kn) in 
@@ -509,7 +510,7 @@ let rec add_term state t=
 	  let b=next uf in
           let trm = constr_of_term t in
 	  let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
-	  let typ = canonize_name typ in
+	  let typ = canonize_name (project state.gls) typ in
 	  let new_node=
 	    match t with
 		Symb _ | Product (_,_) ->
@@ -833,6 +834,7 @@ let complete_one_class state i=
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
 	let _c = pf_unsafe_type_of state.gls
 	  (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
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 62892973d..2ab4dced4 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -219,7 +219,7 @@ let make_prb gls depth additionnal_terms =
 	     | `Nrule patts -> add_quant state id false patts
 	 end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
     begin
-      match atom_of_constr env sigma (EConstr.of_constr (pf_concl gls)) with
+      match atom_of_constr env sigma (pf_concl gls) with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
 	|	`Other g ->
 		  List.iter
@@ -271,7 +271,7 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let type_of t = EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t) in
+  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)
@@ -343,7 +343,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 (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt1)) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
   end }
 
 let refine_exact_check c gl =
@@ -361,7 +361,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 (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt2)) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -385,7 +385,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let trivial = Universes.constr_of_global (Lazy.force _True) in
     let trivial = EConstr.of_constr trivial 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 (Tacmach.New.pf_unsafe_type_of gl 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