diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 12:41:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 12:41:40 +0000 |
| commit | f5bdbc026f6aa9456aa3850451942f72f9c9190e (patch) | |
| tree | 8b31a557397f363758dd70df02e08634079945f1 /theories/Init | |
| parent | d8da8cb7b9af7df65f63af30bfa5775531426165 (diff) | |
Notation eqT superflue
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3816 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init')
| -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 9cebfb7df..fa5ab26f8 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 ?). |