diff options
Diffstat (limited to 'test-suite/success/destruct.v')
| -rw-r--r-- | test-suite/success/destruct.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 7adcc8de30..8013e1d38e 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -67,7 +67,7 @@ Abort. Variable A0:Type. Variable P:A0->Type. Require Import JMeq. -Goal forall a b (p:P a) (q:P b), +Goal forall a b (p:P a) (q:P b), forall H:a = b, eq_rect a P p b H = q -> JMeq (existT _ a p) (existT _ b q). intros. destruct H. |