Merge PR #12588: [exn] Remove some uses of print

Ack-by: gares
Reviewed-by: ppedrot

4 files changed, 21 insertions, 5 deletions

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.ml b/pretyping/reductionops.ml
index 594b8ab54c..fdc770dba6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1085,12 +1085,25 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
+(* NOTE: We absorb anomalies happening in the conversion tactic, which
+   is a bit ugly. This is mostly due to efficiency both in tactics and
+   in the conversion machinery itself. It is not uncommon for a tactic
+   to send some ill-typed term to the engine.
+
+   We would usually say that a tactic that converts ill-typed terms is
+   buggy, but fixing the tactic could have a very large runtime cost
+   *)
+exception AnomalyInConversion of exn
+
+let _ = CErrors.register_handler (function
+    | AnomalyInConversion e ->
+      Some Pp.(str "Conversion test raised an anomaly:" ++
+               spc () ++ CErrors.print e)
+    | _ -> None)
+
 let report_anomaly (e, info) =
   let e =
-    if is_anomaly e then
-      let msg = Pp.(str "Conversion test raised an anomaly:" ++
-                    spc () ++ CErrors.print e) in
-      UserError (None, msg)
+    if is_anomaly e then AnomalyInConversion e
     else e
   in
   Exninfo.iraise (e, info)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 218936edfb..0f288cdd46 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -283,3 +283,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