From 085f52535d2939e18cdd4ae5e6b24a2220465179 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 8 Sep 2010 15:40:17 +0000
Subject: illustrating the wrongness of the current multifile processing for
 coq.

---
 coq/ex/mult2.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/coq/ex/mult2.v b/coq/ex/mult2.v
index 997beefd..81dede72 100644
--- a/coq/ex/mult2.v
+++ b/coq/ex/mult2.v
@@ -1,7 +1,5 @@
-
-
-Require Import mult1.
-
+Require Import Arith.
+Require mult1.
 Definition bar:bool := if le_lt_dec foo 0 then true else false.
 
 
-- 
cgit v1.2.3