Reductionops now return EConstrs.

1 files changed, 3 insertions, 5 deletions

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index f3f19e8542..7ecf0a9e83 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -23,8 +23,6 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
-let compute env sigma c = EConstr.of_constr (compute env sigma c)
-
 let re_sig it  gc = { it = it; sigma = gc; }
 
 (**************************************************************)
@@ -229,13 +227,13 @@ module New = struct
   let pf_reduce_to_quantified_ind gl t =
     pf_apply reduce_to_quantified_ind gl t
 
-  let pf_hnf_constr gl t = EConstr.of_constr (pf_apply hnf_constr gl t)
+  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
-    EConstr.of_constr (pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)))
+    pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))
 
   let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
 
-  let pf_whd_all gl t = EConstr.of_constr (pf_apply whd_all gl t)
+  let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
   let pf_nf_evar gl t = nf_evar (project gl) t