From f7992de2dc4ce0091197b9476779fc120a2fd9ec Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 27 Nov 2018 21:03:57 -0500
Subject: Factor out common code in numeral/string notations

As per https://github.com/coq/coq/pull/8965#issuecomment-441440779
---
 proofs/logic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/logic.ml')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 15ba0a704f..79bd6089a3 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -63,7 +63,7 @@ let catchable_exception = function
   | CErrors.UserError _ | TypeError _
   | Proof.OpenProof _
   (* abstract will call close_proof inside a tactic *)
-  | Notation.NumeralNotationError _
+  | Notation.PrimTokenNotationError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
   (* reduction errors *)
-- 
cgit v1.2.3