diff options
Diffstat (limited to 'theories/Init/Logic.v')
| -rw-r--r-- | theories/Init/Logic.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index d391611dc..1dc998cdf 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -399,14 +399,14 @@ Qed. (* Aliases *) -Notation sym_eq := eq_sym (only parsing). -Notation trans_eq := eq_trans (only parsing). -Notation sym_not_eq := not_eq_sym (only parsing). - -Notation refl_equal := eq_refl (only parsing). -Notation sym_equal := eq_sym (only parsing). -Notation trans_equal := eq_trans (only parsing). -Notation sym_not_equal := not_eq_sym (only parsing). +Notation sym_eq := eq_sym (compat "8.3"). +Notation trans_eq := eq_trans (compat "8.3"). +Notation sym_not_eq := not_eq_sym (compat "8.3"). + +Notation refl_equal := eq_refl (compat "8.3"). +Notation sym_equal := eq_sym (compat "8.3"). +Notation trans_equal := eq_trans (compat "8.3"). +Notation sym_not_equal := not_eq_sym (compat "8.3"). Hint Immediate eq_sym not_eq_sym: core. |