diff options
Diffstat (limited to 'theories/Init/Logic_Type.v')
| -rw-r--r-- | theories/Init/Logic_Type.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 567d2c15c..3244fa14c 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -66,7 +66,7 @@ Defined. Hint Immediate identity_sym not_identity_sym: core. -Notation refl_id := identity_refl (compat "8.3"). -Notation sym_id := identity_sym (compat "8.3"). -Notation trans_id := identity_trans (compat "8.3"). -Notation sym_not_id := not_identity_sym (compat "8.3"). +Notation refl_id := identity_refl (only parsing). +Notation sym_id := identity_sym (only parsing). +Notation trans_id := identity_trans (only parsing). +Notation sym_not_id := not_identity_sym (only parsing). |