diff options
| author | filliatr | 1999-12-12 22:03:12 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-12 22:03:12 +0000 |
| commit | ed8ec17ce48b4d0cf14696a4e9760239aa31f59b (patch) | |
| tree | 6c596c6e8ccebb4d29a856439f07d3fd85a4e3d2 /toplevel/errors.ml | |
| parent | 9658d225b4003ac10c4c670e788d386930c3fa60 (diff) | |
modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
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 af8b7c5cbf..ba1f36cd7c 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -48,9 +48,9 @@ let rec explain_exn_default = function | Sys.Break -> hOV 0 [< 'fNL; 'sTR"User Interrupt." >] - | TypeError(k,ctx,te) -> Himsg.explain_type_error k ctx te + | TypeError(k,ctx,te) -> hOV 0 (Himsg.explain_type_error k ctx te) - | InductiveError e -> Himsg.explain_inductive_error e + | InductiveError e -> hOV 0 (Himsg.explain_inductive_error e) | Stdpp.Exc_located (loc,exc) -> hOV 0 [< if loc = Ast.dummy_loc then [<>] |