diff options
| author | Antonio Nikishaev | 2020-04-01 17:46:55 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-04-30 13:26:00 +0400 |
| commit | b50075866384ee5a35c0fd0147cb607d4e4977d2 (patch) | |
| tree | f6f658d4045e348206324f811735b1db48c17d85 | |
| parent | 5e611ecb1c38860ee5aaa0ccde1bb982ccc43ae4 (diff) | |
do not re-export ListNotations from Program
| -rw-r--r-- | theories/Program/Syntax.v | 3 |
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. |