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