Reductionops API using EConstr.

1 files changed, 14 insertions, 10 deletions

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index e41fb94cc..09f5246ab 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -77,26 +77,27 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
   let sigma = Sigma.Unsafe.of_evar_map (project gls) in
-  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in
+  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma (EConstr.of_constr c) in
   (Sigma.to_evar_map sigma, c)
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_eapply f gls x = 
   on_sig gls (fun evm -> f (pf_env gls) evm x)
 let pf_reduce = pf_apply
+let pf_reduce' f gl c = pf_apply f gl (EConstr.of_constr c)
 let pf_e_reduce = pf_apply
 
-let pf_whd_all         = pf_reduce whd_all
-let pf_hnf_constr                = pf_reduce hnf_constr
-let pf_nf                        = pf_reduce simpl
-let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
-let pf_compute                   = pf_reduce compute
-let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+let pf_whd_all         = pf_reduce' whd_all
+let pf_hnf_constr                = pf_reduce' hnf_constr
+let pf_nf                        = pf_reduce' simpl
+let pf_nf_betaiota               = pf_reduce' (fun _ -> nf_betaiota)
+let pf_compute                   = pf_reduce' compute
+let pf_unfoldn ubinds            = pf_reduce' (unfoldn ubinds)
 let pf_unsafe_type_of            = pf_reduce unsafe_type_of
 let pf_type_of                   = pf_reduce type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
-let pf_conv_x gl                = pf_reduce test_conversion gl Reduction.CONV
+let pf_conv_x gl                = pf_apply test_conversion gl Reduction.CONV
 let pf_conv_x_leq gl            = pf_reduce test_conversion gl Reduction.CUMUL
 let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
 
@@ -158,6 +159,9 @@ module New = struct
   let pf_apply f gl =
     f (Proofview.Goal.env gl) (project gl)
 
+  let pf_reduce f gl c =
+    f (Proofview.Goal.env gl) (project gl) (EConstr.of_constr c)
+
   let of_old f gl =
     f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
 
@@ -217,14 +221,14 @@ module New = struct
     let sigma = project gl in
     nf_evar sigma concl
 
-  let pf_whd_all gl t = pf_apply whd_all gl t
+  let pf_whd_all gl t = pf_reduce whd_all gl t
 
   let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
 
   let pf_reduce_to_quantified_ind gl t =
     pf_apply reduce_to_quantified_ind gl t
 
-  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
+  let pf_hnf_constr gl t = pf_reduce hnf_constr gl t
   let pf_hnf_type_of gl t =
     pf_whd_all gl (pf_get_type_of gl t)