diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Omega.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index 680012462c..5077dc0bd3 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -71,3 +71,11 @@ Lemma lem6 : n=n. Omega. Qed. End C. + +(* Problem of dependencies *) +Require Omega. +Lemma lem7 : (H:O=O->O=O) H=H -> O=O. +Intros; Omega. +Qed. + + |