From 6eede2f5ecc64c82ced0921206bcdcf4efe0bfe8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 10 Jun 2024 15:09:52 +0200 Subject: [PATCH] typing.ml don't produce anomaly when bad relevance warning is AsError This was a mistaken squash of test commit f508cfd968935c16bf38aba21b211b3a3cc9169e AFAICT --- pretyping/typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 2fabc15308fc..153d754117e4 100644 --- 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