From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 02:12:40 +0100
Subject: Evar-normalizing functions now act on EConstrs.

---
 proofs/tacmach.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs/tacmach.ml')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 2fab026eab..3ed262d6e8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -223,7 +223,7 @@ module New = struct
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
-    EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr concl))
+    nf_evar sigma concl
 
   let pf_whd_all gl t = pf_apply whd_all gl t
 
@@ -241,6 +241,6 @@ module New = struct
   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 = EConstr.of_constr (nf_evar (project gl) (EConstr.Unsafe.to_constr t))
+  let pf_nf_evar gl t = nf_evar (project gl) t
 
 end
-- 
cgit v1.2.3