diff options
| author | Gaëtan Gilbert | 2019-05-14 13:10:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-14 13:10:20 +0200 |
| commit | d0e258175280152e504a296a05ecbd1920bb17c9 (patch) | |
| tree | 9e7c80e5792c3769d28b04841651d522c4f5c3f1 /engine | |
| parent | 9f11eeefc204bdad029b66f30bc6c52377af63ae (diff) | |
Fix #10161: occur check when defining an algebraic universe.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/uState.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |