diff options
| author | Jasper Hugunin | 2020-12-15 21:00:29 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2020-12-15 21:00:29 -0800 |
| commit | ef7dbd83b583abf08f162e343250507ad74744a1 (patch) | |
| tree | 5b1af9e274d8136305ed53b98830194979d13dc4 | |
| parent | cd3d7e1384e2b6d929ad4d048810beb3e42f8a98 (diff) | |
Modify Logic/JMeq.v to compile with -mangle-names
| -rw-r--r-- | theories/Logic/JMeq.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 7ee3a99d60..21eed3a696 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -39,8 +39,8 @@ Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. Register JMeq_hom as core.JMeq.hom. Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. -Proof. -intros; destruct H; trivial. +Proof. +intros A B x y H; destruct H; trivial. Qed. #[global] @@ -150,7 +150,7 @@ Lemma JMeq_eq_dep : forall U (P:U->Type) p q (x:P p) (y:P q), p = q -> JMeq x y -> eq_dep U P p x q y. Proof. -intros. +intros U P p q x y H H0. destruct H. apply JMeq_eq in H0 as ->. reflexivity. |