From d0e258175280152e504a296a05ecbd1920bb17c9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 14 May 2019 13:10:20 +0200
Subject: Fix #10161: occur check when defining an algebraic universe.

---
 engine/uState.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'engine/uState.ml')

diff --git a/engine/uState.ml b/engine/uState.ml
index adea78d4c9..9b27ff7916 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -214,7 +214,8 @@ let process_universe_constraints ctx cstrs =
   | Inr l, Inl r | Inl r, Inr l ->
     let alg = LSet.mem l ctx.uctx_univ_algebraic in
     let inst = univ_level_rem l r r in
-      if alg then (instantiate_variable l inst vars; local)
+      if alg && not (LSet.mem l (Universe.levels inst)) then
+        (instantiate_variable l inst vars; local)
       else
         let lu = Universe.make l in
         if univ_level_mem l r then
-- 
cgit v1.2.3