diff options
| author | Jan-Oliver Kaiser | 2020-05-14 17:08:20 +0200 |
|---|---|---|
| committer | Pierre Roux | 2021-04-22 09:16:22 +0200 |
| commit | 2cbc36c6ae4ca22e000dbb045c865f54a454aca3 (patch) | |
| tree | 28cfb03cc4af70bcd86f7058571aa5a44da270b0 /theories | |
| parent | 3442bfa0e7c7e5ba3ce7d62f16d221c2e6da03cf (diff) | |
Enable canonical `fun _ => _` projections.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/ssr/ssrbool.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index d8eb005ab2..72e6e757d3 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -297,7 +297,6 @@ Require Import ssreflect ssrfun. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Set Warnings "-projection-no-head-constant". Notation reflect := Bool.reflect. Notation ReflectT := Bool.ReflectT. @@ -1227,7 +1226,9 @@ Definition clone_pred T U := Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ id) : form_scope. Canonical predPredType T := PredType (@id (pred T)). +Set Warnings "-redundant-canonical-projection". Canonical boolfunPredType T := PredType (@id (T -> bool)). +Set Warnings "redundant-canonical-projection". (** The type of abstract collective predicates. While {pred T} is contertible to pred T, it presents the pred_sort coercion |