Nettoyage suite à la détection par défaut des variables inutilisées par ocaml 3.09

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

5 files changed, 6 insertions, 7 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 1b48acf04..bb66d3f26 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -147,7 +147,7 @@ let load_constant i ((sp,kn),(_,_,_,kind)) =
 let open_constant i ((sp,kn),_) =
   Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
 
-let cache_constant ((sp,kn),(cdt,dhyps,imps,kind) as o) =
+let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   if Idmap.mem id !vartab then
@@ -211,7 +211,7 @@ let hcons_constant_declaration = function
 
 let declare_constant_common id dhyps (cd,kind) =
   let imps = implicits_flags () in
-  let (sp,kn as oname) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in
+  let (sp,kn) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in
   let kn = constant_of_kn kn in
   kn
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 69aea75f8..250411e6b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -572,7 +572,6 @@ let library_cache = Hashtbl.create 17
 
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
-  let prefix = dir, (mp, empty_dirpath) in
   let substobjs, objects =
     try 
       ignore(Global.lookup_module mp);
diff --git a/library/impargs.ml b/library/impargs.ml
index f41d26c99..abf583d99 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -143,7 +143,7 @@ let update pos rig (na,st) =
       | Some (DepFlexAndRigid (fpos,rpos) as x) ->
           if argument_less (pos,fpos) or pos=fpos then DepRigid pos else
           if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x
-      | Some (DepFlex fpos as x) ->
+      | Some (DepFlex fpos) ->
           if argument_less (pos,fpos) or pos=fpos then DepRigid pos
           else DepFlexAndRigid (fpos,pos)
       | Some Manual -> assert false
diff --git a/library/lib.ml b/library/lib.ml
index b8e7cea95..b1896ae5e 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -50,7 +50,7 @@ let subst_objects prefix subst seg =
 let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
-    | ((sp,kn as oname),Leaf o) as node :: stk -> 
+    | ((sp,kn as oname),Leaf o) :: stk -> 
 	let id = id_of_label (label kn) in
 	  (match classify_object (oname,o) with 
 	     | Dispose -> clean acc stk
diff --git a/library/nametab.ml b/library/nametab.ml
index 0ce45c4fb..ddd06c0c2 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -96,7 +96,7 @@ struct
      [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)
 
   let rec push_until uname o level (current,dirmap) = function
-    | modid :: path as dir ->
+    | modid :: path ->
 	let mc = 
 	  try ModIdmap.find modid dirmap
 	  with Not_found -> (Nothing, ModIdmap.empty)
@@ -135,7 +135,7 @@ struct
 
 
 let rec push_exactly uname o level (current,dirmap) = function
-  | modid :: path as dir ->
+  | modid :: path ->
       let mc = 
 	try ModIdmap.find modid dirmap
 	with Not_found -> (Nothing, ModIdmap.empty)