Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 11 insertions, 11 deletions

diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
index d3e98ae4..57878a5f 100644
--- a/test-suite/modules/Nat.v
+++ b/test-suite/modules/Nat.v
@@ -1,19 +1,19 @@
-Definition T:=nat.
+Definition T := nat.
 
-Definition le:=Peano.le.
+Definition le := le.
 
-Hints Unfold le.
+Hint Unfold le.
 
-Lemma le_refl:(n:nat)(le n n).
-  Auto.
+Lemma le_refl : forall n : nat, le n n.
+  auto.
 Qed.
 
-Require Le.
+Require Import Le.
 
-Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
-  EAuto with arith.
+Lemma le_trans : forall n m k : nat, le n m -> le m k -> le n k.
+   eauto with arith.
 Qed.
 
-Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m.
-  EAuto with arith.
-Qed.
+Lemma le_antis : forall n m : nat, le n m -> le m n -> n = m.
+   eauto with arith.
+Qed.
\ No newline at end of file