From 6296cc78d9809c501273c5020ae1d7c53bf9c5ed Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Sep 2014 16:48:23 +0200 Subject: fix test-suite/success/decl_mode.v --- test-suite/success/decl_mode.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- cgit v1.2.3