Merge PR coq#19195: typing.ml don't produce anomaly when bad relevanc…

…e warning is AsError Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Jun 11, 2024 · 58d8ec3 · 58d8ec3
2 parents ea11254 + 6eede2f
commit 58d8ec3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
@@ -411,7 +411,7 @@ let warn_bad_relevance_binder ?loc env sigma rlv bnd =
 | CWarnings.Disabled | CWarnings.Enabled ->
   CWarnings.warn bad_relevance_msg ?loc (env,sigma,Typeops.BadRelevanceBinder (rlv, bnd))
 | CWarnings.AsError ->
-  CErrors.anomaly (CErrors.print (PretypeError (env, sigma, TypingError (Type_errors.BadBinderRelevance (rlv, bnd)))))
+  Loc.raise ?loc (PretypeError (env, sigma, TypingError (Type_errors.BadBinderRelevance (rlv, bnd))))
 
 type relevance_preunify =
   | Trivial