diff options
Diffstat (limited to 'test-suite/success/decl_mode.v')
| -rw-r--r-- | test-suite/success/decl_mode.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v index 52575eca..58f79d45 100644 --- a/test-suite/success/decl_mode.v +++ b/test-suite/success/decl_mode.v @@ -67,7 +67,7 @@ proof. end proof. Qed. -Require Omega. +Require Import Omega. Lemma even_double_n: (forall m, even (double m)). proof. |