From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 8 Nov 2016 19:02:40 +0100
Subject: Pretyping API using EConstr.

---
 proofs/logic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/logic.ml')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 93b31ced1..093d949d5 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -314,7 +314,7 @@ let check_meta_variables c =
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let evm, b = Reductionops.infer_conv env sigma ty conclty in
+    let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
       if b then evm 
       else raise (RefinerError (BadType (arg,ty,conclty)))
   else sigma
-- 
cgit v1.2.3