From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/success/decl_mode.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/success/decl_mode.v') 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. -- cgit v1.2.3