diff options
| -rw-r--r-- | theories/Init/Logic_TypeSyntax.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index 9cebfb7df9..fa5ab26f8a 100644 --- a/theories/Init/Logic_TypeSyntax.v +++ b/theories/Init/Logic_TypeSyntax.v @@ -15,8 +15,6 @@ Require Logic_Type. Notation "x == y" := (eq ? x y) (at level 5, no associativity, only parsing). Notation "x === y" := (identityT ? x y) (at level 5, no associativity). -Notation "'eqT'" := eq (at level 0). - (* Order is important to give printing priority to fully typed ALL and EX *) Notation AllT := (all ?). |