From 2bdd0f98ea8fa2444e4198d7be160a189aa5f933 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Feb 2019 16:13:14 +0100
Subject: Remove the Plexing.Error exception.

This was dead code, it was never raised ever.
---
 vernac/explainErr.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'vernac')

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.")
-- 
cgit v1.2.3