diff options
| author | Gaëtan Gilbert | 2019-10-02 14:29:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-02 14:29:31 +0200 |
| commit | 08740d8e5a6974183e13b4cf372caade1c25f6fa (patch) | |
| tree | f2d5ce163f9a990ecf5181bd628dae9acdad7087 | |
| parent | 004d7aeeca9f5ae4ceb9f109fa90a87e58457680 (diff) | |
simplify branch in process_universe_constraints
| -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 |