aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--theories/Program/Syntax.v3
1 files changed, 0 insertions, 3 deletions
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 03401aea2b..7a8ddbe71e 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -30,7 +30,4 @@ Arguments snd {A B} _.
Arguments nil {A}.
Arguments cons {A} _ _.
-Require List.
-Export List.ListNotations.
-
Require Import Bvector.