diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index 0fed4be4b835..add970edb2cb 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -15,8 +15,6 @@ Require Bool. Require Import ssreflect ssrfun. -#[export] Set Warnings "-overwriting-delimiting-key". - (** A theory of boolean predicates and operators. A large part of this file is concerned with boolean reflection. @@ -468,7 +466,9 @@ Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format "'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'"). (** Shorter delimiter **) +#[export] Set Warnings "-overwriting-delimiting-key". Delimit Scope bool_scope with B. +#[export] Set Warnings "overwriting-delimiting-key". Open Scope bool_scope. (** An alternative to xorb that behaves somewhat better wrt simplification. **)