diff options
Diffstat (limited to 'toplevel/errors.ml')
| -rw-r--r-- | toplevel/errors.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/errors.ml b/toplevel/errors.ml index c72f2ddb3c..6c76e5e888 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -55,6 +55,8 @@ let rec explain_exn_default = function hOV 0 [< 'sTR "Anomaly: Invalid argument "; 'sTR (guill s); report () >] | Sys.Break -> hOV 0 [< 'fNL; 'sTR"User Interrupt." >] + | Univ.UniverseInconsistency -> + hOV 0 [< 'sTR "Error: Universe Inconsistency." >] | TypeError(k,ctx,te) -> hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error k ctx te >] | InductiveError e -> |