diff options
| -rw-r--r-- | engine/uState.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 5ebac4b817..d93ccafcf0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -244,9 +244,7 @@ let process_universe_constraints ctx cstrs = | Some r' -> if Level.is_small r' then if not (Universe.is_levels l) - then - if UGraph.check_leq univs l r then local - else + then (* l contains a +1 and r=r' small so l <= r impossible *) raise (UniverseInconsistency (Le, l, r, None)) else if UGraph.check_leq univs l r then match Univ.Universe.level l with |