From 390fd4ac0a969103caeb5db3e5138e26f9a533de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Nov 2016 17:49:11 +0100
Subject: Chasing a few unsafe constr coercions.

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

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 4b027a1273..97c5cda770 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -41,10 +41,8 @@ let project  = Refiner.project
 let pf_env   = Refiner.pf_env
 let pf_hyps  = Refiner.pf_hyps
 
-let test_conversion cb env sigma c1 c2 =
-  let c1 = EConstr.Unsafe.to_constr c1 in
-  let c2 = EConstr.Unsafe.to_constr c2 in
-  test_conversion cb env sigma c1 c2
+let test_conversion env sigma pb c1 c2 =
+  Reductionops.check_conv ~pb env sigma c1 c2
 
 let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
 let pf_hyps_types gls  =
-- 
cgit v1.2.3