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 +
 pretyping/pretyping.mllib   | 2 +-
 pretyping/reductionops.mli  | 2 ++
 3 files changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping')

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
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 07154d4e03..c31ecc135c 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,8 +1,8 @@
 Geninterp
 Locus
 Locusops
-Pretype_errors
 Reductionops
+Pretype_errors
 Inductiveops
 Arguments_renaming
 Retyping
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b316b3c213..f8c9af7cad 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -293,3 +293,5 @@ val whd_betaiota_deltazeta_for_iota_state :
 (** {6 Meta-related reduction functions } *)
 val meta_instance : env -> evar_map -> constr freelisted -> constr
 val nf_meta       : env -> evar_map -> constr -> constr
+
+exception AnomalyInConversion of exn
-- 
cgit v1.2.3