aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Bool')
-rwxr-xr-xtheories/Bool/Bool.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index afc9840e1..96160f091 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -175,6 +175,7 @@ Definition negb := [b:bool]Cases b of
Infix "||" orb (at level 4, left associativity) : bool_scope.
Infix "&&" andb (at level 3, left associativity) : bool_scope.
Notation "!! b" := (negb b) (at level 0, right associativity) : bool_scope.
+Open Scope bool_scope.
(**************************)
(** Lemmas about [negb] *)