Nettoyage argument de nil

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4639 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 12 insertions, 9 deletions

diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 77f943716..4b7083c0a 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -19,6 +19,7 @@
 Require PolyList.
 
 Set Implicit Arguments.
+V7only [Implicits nil [1].].
 
 Section first_definitions.
 
@@ -27,11 +28,11 @@ Section first_definitions.
 
   Definition set := (list A).
 
-  Definition empty_set := (nil ?) : set.
+  Definition empty_set := (!nil ?) : set.
 
   Fixpoint set_add [a:A; x:set] : set :=
     Cases x of
-    | nil => (cons a (nil A))
+    | nil => (cons a nil)
     | (cons a1 x1) => Cases (Aeq_dec a a1) of 
                     | (left _) => (cons a1 x1) 
                     | (right _) => (cons a1 (set_add a x1))
@@ -60,7 +61,7 @@ Section first_definitions.
 
   Fixpoint set_inter [x:set] : set -> set :=
     Cases x of
-    | nil => [y](nil A)
+    | nil => [y]nil
     | (cons a1 x1) => [y]if (set_mem a1 y) 
                       then (cons a1 (set_inter x1 y))
 		      else (set_inter x1 y)
@@ -75,7 +76,7 @@ Section first_definitions.
   (** returns the set of all els of [x] that does not belong to [y] *)
   Fixpoint set_diff [x:set] : set -> set :=
     [y]Cases x of
-    | nil => (nil A)
+    | nil => nil
     | (cons a1 x1) => if (set_mem a1 y) 
                       then (set_diff x1 y)
 		      else (set_add a1 (set_diff x1 y))
@@ -384,4 +385,5 @@ Section other_definitions.
  
 End other_definitions.
 
+V7only [Implicits nil [].].
 Unset Implicit Arguments.
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 450fedfc6..4168655fe 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -494,7 +494,6 @@ End Reverse_Induction.
 End Lists.
 
 Implicits nil [1].
-V7only [Implicits nil [].].
 
 Hints Resolve nil_cons app_nil_end ass_app app_ass : datatypes v62.
 Hints Resolve app_comm_cons  app_cons_not_nil : datatypes v62.
@@ -517,7 +516,7 @@ Variables A,B:Set.
 Variable  f:A->B.
 Fixpoint map [l:(list A)] : (list B) :=
   Cases l of 
-     nil       => (nil B)
+     nil       => nil
   | (cons a t) => (cons (f a) (map t))
   end.
 End Map.
@@ -535,13 +534,13 @@ Qed.
 
 Fixpoint flat_map [A,B:Set; f:A->(list B); l:(list A)] : (list B) :=
   Cases l of
-    nil => (nil B)
+    nil => nil
   | (cons x t) => (app (f x) (flat_map f t))
   end.
 
 Fixpoint list_prod [A:Set; B:Set; l:(list A)] : (list B)->(list A*B) :=
   [l']Cases l of
-    nil => (nil A*B)
+    nil => nil
   | (cons x t) => (app (map [y:B](x,y) l')
       	       	       	     (list_prod t l'))
   end.
@@ -574,7 +573,7 @@ Qed.
 
 Fixpoint list_power [A,B:Set; l:(list A)] : (list B)->(list (list A*B)) :=
   [l']Cases l of
-    nil => (cons (nil A*B) (nil ?))
+    nil => (cons nil nil)
   | (cons x t) => (flat_map [f:(list A*B)](map [y:B](cons (x,y) f) l') 
       	       	       	    (list_power t l'))
   end.
@@ -632,6 +631,8 @@ Qed.
 
 End Functions_on_lists.
 
+V7only [Implicits nil [].].
+
 (** Exporting list notations *)
 
 V8Infix "::" cons (at level 45, right associativity) : list_scope.