From 4a4d35baf47944f4d30bd10de7e71f46f17da8f2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 15 Jul 2020 17:33:04 +0200
Subject: [gramlib] Remove legacy located exception wrapper in favor of
 standard infrastructure.

The old wrapper was basically unused, this PR also fixes backtraces in
some class of bugs such as https://github.com/coq/coq/issues/12695
---
 plugins/ssr/ssrcommon.ml | 3 +--
 plugins/ssr/ssrelim.ml   | 1 -
 2 files changed, 1 insertion(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 65204b7868..9e120aee87 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1124,8 +1124,7 @@ let tclDO n tac =
       let _, info = Exninfo.capture e in
       let e' = CErrors.UserError (l, prefix i ++ s) in
       Exninfo.iraise (e', info)
-    | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s))  ->
-      raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+  in
   let rec loop i gl =
     if i = n then tac_err_at i gl else
     (tclTHEN (tac_err_at i) (loop (i + 1))) gl in
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index a12b4aad11..1c81fbc10b 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -490,7 +490,6 @@ let equality_inj l b id c =
   let msg = ref "" in
   try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
   with
-    | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s))
     | CErrors.UserError (_,s)
   when msg := Pp.string_of_ppcmds s;
        !msg = "Not a projectable equality but a discriminable one." ||
-- 
cgit v1.2.3