aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 09:03:46 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 09:03:46 +0100
commit2189505b6e50c9a9aa8e9d520c05461e59f18d04 (patch)
tree0aa4f9795081d0c8199f3350a6a2dafc5ce2fd05
parent66ad590733b3a4dafe3c55a0b59d4f13f6c4b7bc (diff)
parentd7abadbef61ab0d45ffc5a5a45ff31bd39103446 (diff)
Merge PR#392: strengthened the statement of JMeq_eq_dep
-rw-r--r--theories/Logic/JMeq.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 2f95856b4..86d05e8fb 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -130,7 +130,7 @@ Qed.
is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *)
Lemma JMeq_eq_dep :
- forall U (P:U->Prop) p q (x:P p) (y:P q),
+ 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.