diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2010-09-08 15:40:17 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2010-09-08 15:40:17 +0000 |
| commit | 085f52535d2939e18cdd4ae5e6b24a2220465179 (patch) | |
| tree | 37b6ea61c0bc40651a07e2c9af0b2a8a63373935 /coq/ex/mult2.v | |
| parent | 6c2e5a4b4302619aa46089101b40102fee7a9b6b (diff) | |
illustrating the wrongness of the current multifile processing for coq.
Diffstat (limited to 'coq/ex/mult2.v')
| -rw-r--r-- | coq/ex/mult2.v | 6 |
1 files 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. |