diff --git a/peano_nat.mlw b/peano_nat.mlw
index cae2d2d4aa3ed134789064fa8670678ff22664f5..6690f3b7c671594f06b6005c6d402e0ad649b86b 100644
--- a/peano_nat.mlw
+++ b/peano_nat.mlw
@@ -48,7 +48,7 @@ end
 
 module Add
 
-  use import Nat
+  use Nat
   
   goal plus_ol: 
     forall n. O + n = n
@@ -107,9 +107,9 @@ end
 
 module Compare
 
-  use import Nat
-  (* use import Add *)
-  (* use import Inconsistency *)
+  use Nat
+  use Add
+  (* use Inconsistency *)
  
   inductive le nat nat = 
   | Le_n : forall n:nat. le n n
@@ -132,8 +132,8 @@ end
 
 
 module Sub
- use import Nat
- use import Compare
+ use Nat
+ use Compare
  
  function sub (n m:nat) : nat =
  match n, m with
@@ -173,4 +173,4 @@ module Sub
  lemma sub_lt_nm:forall n m. ... -> sub n m < n
    
  *)
-end	
\ No newline at end of file
+end