From d2ca1efe969ece40254ba19281964c7f391f3f99 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 27 Jun 2020 16:26:17 +0200
Subject: [error handling] Anomaly in Conversion is a "precatchable_exception"

This is just a fixup, likely all the places that are matching on
`UserErr` directly are just buggy.
---
 pretyping/pretype_errors.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 414663c826..207ffc7b86 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -66,6 +66,7 @@ exception PretypeError of env * Evd.evar_map * pretype_error
 
 let precatchable_exception = function
   | CErrors.UserError _ | TypeError _ | PretypeError _
+  | Reductionops.AnomalyInConversion _
   | Nametab.GlobalizationError _ -> true
   | _ -> false
 
-- 
cgit v1.2.3