Merge PR #9479: Remove the Plexing.Error exception.

Reviewed-by: ejgallego

5 files changed, 1 insertions, 12 deletions

diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 0ad11d075f..e959e9b9e6 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -663,13 +663,8 @@ let init_entry_functions entry =
        entry.econtinue <- f; f lev bp a strm)
 
 let extend_entry ~warning entry position rules =
-  try
     let elev = Gramext.levels_of_rules ~warning entry position rules in
     entry.edesc <- Dlevels elev; init_entry_functions entry
-  with Plexing.Error s ->
-    Printf.eprintf "Lexer initialization error:\n- %s\n" s;
-    flush stderr;
-    failwith "Grammar.extend"
 
 (* Deleting a rule *)
 
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index f99a3c2480..fce5445ad8 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -4,8 +4,6 @@
 
 type pattern = string * string
 
-exception Error of string
-
 type location_function = int -> Loc.t
 type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
 
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index eed4082e00..6139dc4020 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -19,9 +19,6 @@ type pattern = string * string
 -      The way tokens patterns are interpreted to parse tokens is done
        by the lexer, function [tok_match] below. *)
 
-exception Error of string
-    (** A lexing error exception to be used by lexers. *)
-
 (** Lexer type *)
 
 type 'te lexer =
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index cdbe444e5b..e933f08735 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -256,7 +256,7 @@ let rec discard_to_dot () =
   try
     Pcoq.Entry.parse parse_to_dot top_buffer.tokens
   with
-    | Gramlib.Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot ()
+    | CLexer.Error.E _ -> discard_to_dot ()
     | e when CErrors.noncritical e -> ()
 
 let read_sentence ~state input =
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 71770a21ca..42b313f200 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -28,7 +28,6 @@ exception EvaluatedError of Pp.t * exn option
 let explain_exn_default = function
   (* Basic interaction exceptions *)
   | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
-  | Gramlib.Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
   | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err))
   | Sys_error msg -> hov 0 (str "System error: " ++ guill msg)
   | Out_of_memory -> hov 0 (str "Out of memory.")