aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--theories/Bool/Bool.v7
1 files changed, 0 insertions, 7 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index bae2e14ab..2995f0515 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -723,10 +723,3 @@ Proof.
Qed.
-(** Compatibility *)
-
-Notation andb := Datatypes.andb (only parsing).
-Notation orb := Datatypes.orb (only parsing).
-Notation implb := Datatypes.implb (only parsing).
-Notation xorb := Datatypes.xorb (only parsing).
-Notation negb := Datatypes.negb (only parsing).