From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 10 Nov 2016 11:39:27 +0100
Subject: Unification API using EConstr.

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

(limited to 'proofs/refine.ml')

diff --git a/proofs/refine.ml b/proofs/refine.ml
index 19134bfa3..0ed74c9b3 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -98,7 +98,7 @@ let make_refine_enter ?(unsafe = true) f =
   let self = Proofview.Goal.goal gl in
   let _ =
     if not (Evarutil.occur_evar_upto sigma self c) then ()
-    else Pretype_errors.error_occur_check env sigma self c
+    else Pretype_errors.error_occur_check env sigma self (EConstr.of_constr c)
   in
   (** Proceed to the refinement *)
   let sigma = match evkmain with
-- 
cgit v1.2.3