diff options
| -rw-r--r-- | checker/checker.ml | 4 | ||||
| -rw-r--r-- | checker/univ.ml | 5 |
2 files changed, 5 insertions, 4 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index d3d114d7d7..8a5220c9ca 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -243,7 +243,9 @@ let explain_exn = function | Invalid_argument s -> hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ()) | Sys.Break -> - hov 0 (fnl () ++ str "User interrupt.") + hov 0 (fnl () ++ str "User interrupt.") + | Univ.AlreadyDeclared -> + hov 0 (str "Error: Multiply declared universe.") | Univ.UniverseInconsistency (o,u,v) -> let msg = if !Flags.debug (*!Constrextern.print_universes*) then diff --git a/checker/univ.ml b/checker/univ.ml index e50e883adf..a0511ad21b 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1088,14 +1088,13 @@ let subst_univs_universe fn ul = let merge_context strict ctx g = let g = Array.fold_left - (* Be lenient, module typing reintroduces universes and - constraints due to includes *) - (fun g v -> try add_universe v strict g with AlreadyDeclared -> g) + (fun g v -> add_universe v strict g) g (UContext.instance ctx) in merge_constraints (UContext.constraints ctx) g let merge_context_set strict ctx g = let g = LSet.fold + (* Include and side effects still have double-declared universes *) (fun v g -> try add_universe v strict g with AlreadyDeclared -> g) (ContextSet.levels ctx) g in merge_constraints (ContextSet.constraints ctx) g |