diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml (renamed from toplevel/errors.ml) | 0 | ||||
| -rw-r--r-- | toplevel/cerrors.mli (renamed from toplevel/errors.mli) | 0 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 4 | ||||
| -rw-r--r-- | toplevel/protectedtoplevel.ml | 4 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 8 |
5 files changed, 8 insertions, 8 deletions
diff --git a/toplevel/errors.ml b/toplevel/cerrors.ml index da9ae4a4de..da9ae4a4de 100644 --- a/toplevel/errors.ml +++ b/toplevel/cerrors.ml diff --git a/toplevel/errors.mli b/toplevel/cerrors.mli index 2207608a87..2207608a87 100644 --- a/toplevel/errors.mli +++ b/toplevel/cerrors.mli diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b273034df9..c174877dff 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -206,9 +206,9 @@ let parse_args () = try Stream.empty s; exit 1 with Stream.Failure -> - msgnl (Errors.explain_exn e); exit 1 + msgnl (Cerrors.explain_exn e); exit 1 end - | e -> begin msgnl (Errors.explain_exn e); exit 1 end + | e -> begin msgnl (Cerrors.explain_exn e); exit 1 end (* To prevent from doing the initialization twice *) diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml index 730b6768db..0e28a8373f 100644 --- a/toplevel/protectedtoplevel.ml +++ b/toplevel/protectedtoplevel.ml @@ -55,7 +55,7 @@ let acknowledge_command_ref = str "successfully executed " ++ int command_count ++ fnl () ++ str "error message" ++ fnl () ++ (match opt_exn with - Some e -> Errors.explain_exn e + Some e -> Cerrors.explain_exn e | None -> (mt ())) ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ())) @@ -151,7 +151,7 @@ let rec parse_one_command_group input_channel = let protected_loop input_chan = let rec explain_and_restart e = begin - output_results_nl(Errors.explain_exn e); + output_results_nl(Cerrors.explain_exn e); rearm_break(); looprec input_chan; end diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 8bd6ba8e4a..29c0e60551 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -11,7 +11,7 @@ open Pp open Util open Options -open Errors +open Cerrors open Vernac open Pcoq open Protectedtoplevel @@ -124,7 +124,7 @@ let print_highlight_location ib (bp,ep) = str sn ++ str dn) in (l1 ++ li ++ ln) in - (str"Toplevel input, characters " ++ Errors.print_loc (bp,ep) ++ fnl () ++ + (str"Toplevel input, characters " ++ Cerrors.print_loc (bp,ep) ++ fnl () ++ highlight_lines ++ fnl ()) (* Functions to report located errors in a file. *) @@ -147,7 +147,7 @@ let print_location_in_file s fname (bp,ep) = let (line, bol) = line_of_pos 1 0 0 in close_in ic; (errstrm ++ str", line " ++ int line ++ - str", characters " ++ Errors.print_loc (bp-bol,ep-bol) ++ fnl ()) + str", characters " ++ Cerrors.print_loc (bp-bol,ep-bol) ++ fnl ()) with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ())) let print_command_location ib dloc = @@ -235,7 +235,7 @@ let print_toplevel_error exc = raise Vernacinterp.Quit | _ -> (if is_pervasive_exn exc then (mt ()) else locstrm) ++ - Errors.explain_exn exc + Cerrors.explain_exn exc (* Read the input stream until a dot is encountered *) let parse_to_dot = |