From 26af31cb46c7baf92325dd22bf6ee33aaa2172d2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 14 Oct 2015 18:17:42 +0200
Subject: Occur-check in evar_define was not strong enough.

---
 pretyping/evarsolve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 754ad8f588..bbc4f1db29 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1484,7 +1484,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
     if occur_meta body then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar evk body then raise (OccurCheckIn (evd',body));
+    if occur_evar_upto evd' evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
     let evd', body = refresh_universes pbty env evd' body in
 (* Cannot strictly type instantiations since the unification algorithm
-- 
cgit v1.2.3