diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-16 16:48:23 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-16 16:48:23 +0200 |
| commit | 6296cc78d9809c501273c5020ae1d7c53bf9c5ed (patch) | |
| tree | 966e0bbf67f8e078401e84020367cdff66ac7454 | |
| parent | 2e1b90f8b0a585c4a4dd65ffd4b297442cc66cc8 (diff) | |
fix 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 52575eca5..58f79d45e 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. |