diff options
Diffstat (limited to 'toplevel/errors.ml')
| -rw-r--r-- | toplevel/errors.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/errors.ml b/toplevel/errors.ml index cf48f0764..623ebbfbb 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -65,8 +65,8 @@ let rec explain_exn_default = function 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 >] + | TypeError(ctx,te) -> + hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error ctx te >] | PretypeError(ctx,te) -> hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_pretype_error ctx te >] | InductiveError e -> |