diff options
Diffstat (limited to 'test-suite/failure/Uminus.v')
| -rw-r--r-- | test-suite/failure/Uminus.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v index 6866f19a..3c3bf375 100644 --- a/test-suite/failure/Uminus.v +++ b/test-suite/failure/Uminus.v @@ -31,7 +31,7 @@ Lemma Omega : forall i:U -> prop, induct i -> up (i WF). Proof. intros i y. apply y. -unfold le, WF, induct in |- *. +unfold le, WF, induct. intros x H0. apply y. exact H0. @@ -39,7 +39,7 @@ Qed. Lemma lemma1 : induct (fun u => down (I u)). Proof. -unfold induct in |- *. +unfold induct. intros x p. intro q. apply (q (fun u => down (I u)) p). |