diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/JMeq.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 25b7811417..3914f44a2c 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -31,7 +31,7 @@ Arguments JMeq_refl {A x} , [A] x. Register JMeq as core.JMeq.type. Register JMeq_refl as core.JMeq.refl. -Hint Resolve JMeq_refl. +Hint Resolve JMeq_refl : core. Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. @@ -42,7 +42,7 @@ Proof. intros; destruct H; trivial. Qed. -Hint Immediate JMeq_sym. +Hint Immediate JMeq_sym : core. Register JMeq_sym as core.JMeq.sym. |