typing.ml don't produce anomaly when bad relevance warning is AsError

This was a mistaken squash of test commit f508cfd AFAICT
SkySkimmer · Jun 10, 2024 · 6eede2f · 6eede2f
1 parent f37ff96
commit 6eede2f
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