diff options
| author | coqbot-app[bot] | 2021-04-23 14:48:49 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-23 14:48:49 +0000 |
| commit | d332bbc3c1118631eb8c935ba61a8d071a90428e (patch) | |
| tree | b7b63655bdd186d7a9d11a0bf73268de5b186599 /theories | |
| parent | a0c3ebf4a6357a5140b98b4b40c71133c53d802e (diff) | |
| parent | 82910bed2fccee7d1f4814e3339fbae374980e68 (diff) | |
Merge PR #14041: Enable canonical fun _ => _ projections.
Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
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 |