From e4f066238799a4598817dfeab8a044760ab670de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 7 Nov 2016 20:33:06 +0100
Subject: Coercion API using EConstr.

---
 proofs/clenv.ml  | 2 +-
 proofs/refine.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index c2130a64a3..0515e41986 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -670,7 +670,7 @@ let define_with_type sigma env ev c =
   let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in
   let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let j = Environ.make_judge c ty in
-  let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
+  let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in
   let (ev, _) = destEvar ev in
   let sigma = Evd.define ev j.Environ.uj_val sigma in
   sigma
diff --git a/proofs/refine.ml b/proofs/refine.ml
index b62f0bea48..19134bfa34 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -136,7 +136,7 @@ let with_type env evd c t =
   let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in
   let j = Environ.make_judge c my_type in
   let (evd,j') =
-    Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+    Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t)
   in
   evd , j'.Environ.uj_val
 
-- 
cgit v1.2.3