Cleaning opening of the standard List module.

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

6 files changed, 150 insertions, 156 deletions

diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index 1604b0eb1..1a41ec70b 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -55,7 +55,6 @@ struct
 end
 open M
 
-open List
 open Mutils
 
 
@@ -122,7 +121,7 @@ let real_nonlinear_prover d l =
     match kd with
      | Axiom_lt i -> poly_mul p y
      | Axiom_eq i -> poly_mul (poly_pow p 2) y
-     |   _        -> failwith "monoids") m (poly_const (Int 1)) , map  snd m))
+     |   _        -> failwith "monoids") m (poly_const (Int 1)) , List.map snd m))
    (sets_of_list neq) in
 
   let (cert_ideal, cert_cone,monoid) = deepen_until d (fun d ->
@@ -130,10 +129,10 @@ let real_nonlinear_prover d l =
     real_positivnullstellensatz_general false d peq pge (poly_neg (fst m) ) in
 		      (ci,cc,snd m)) monoids) 0 in
 
-  let proofs_ideal = map2 (fun q i -> Eqmul(term_of_poly q,Axiom_eq i))
+  let proofs_ideal = List.map2 (fun q i -> Eqmul(term_of_poly q,Axiom_eq i))
    cert_ideal (List.map snd eq) in
 
-  let proofs_cone = map term_of_sos cert_cone in
+  let proofs_cone = List.map term_of_sos cert_cone in
 
   let proof_ne =
    let (neq , lt) = List.partition
@@ -159,7 +158,7 @@ let pure_sos  l =
  (* If there is no strict inequality,
     I should nonetheless be able to try something - over Z  > is equivalent to -1  >= *)
  try
-  let l = List.combine l (interval 0 (length l -1)) in
+  let l = List.combine l (interval 0 (List.length l -1)) in
   let (lt,i) =  try (List.find (fun (x,_) -> snd x =  Mc.Strict) l)
    with Not_found -> List.hd l in
   let plt = poly_neg (poly_of_term (expr_to_term (fst lt))) in
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 6ddc48e73..130f6bfd4 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -10,7 +10,6 @@
 (* Nonlinear universal reals procedure using SOS decomposition.              *)
 (* ========================================================================= *)
 open Num;;
-open List;;
 open Sos_types;;
 open Sos_lib;;
 
@@ -40,7 +39,7 @@ let decimalize =
     let z = pow10(-e) */ y +/ Int 1 in
     let k = round_num(pow10 d */ z) in
     (if x </ Int 0 then "-0." else "0.") ^
-    implode(tl(explode(string_of_num k))) ^
+    implode(List.tl(explode(string_of_num k))) ^
     (if e = 0 then "" else "e"^string_of_int e);;
 
 (* ------------------------------------------------------------------------- *)
@@ -123,7 +122,7 @@ let vector_dot (v1:vector) (v2:vector) =
         (combine ( */ ) (fun x -> x =/ Int 0) (snd v1) (snd v2));;
 
 let vector_of_list l =
-  let n = length l in
+  let n = List.length l in
   (n,itlist2 (|->) (1--n) l undefined :vector);;
 
 (* ------------------------------------------------------------------------- *)
@@ -176,9 +175,9 @@ let diagonal (v:vector) =
   ((n,n),foldl (fun a i c -> ((i,i) |-> c) a) undefined (snd v) : matrix);;
 
 let matrix_of_list l =
-  let m = length l in
+  let m = List.length l in
   if m = 0 then matrix_0 (0,0) else
-  let n = length (hd l) in
+  let n = List.length (List.hd l) in
   (m,n),itern 1 l (fun v i -> itern 1 v (fun c j -> (i,j) |-> c)) undefined;;
 
 (* ------------------------------------------------------------------------- *)
@@ -302,14 +301,14 @@ let string_of_vector min_size max_size (v:vector) =
   let n_raw = dim v in
   if n_raw = 0 then "[]" else
   let n = max min_size (min n_raw max_size) in
-  let xs = map ((o) string_of_num (element v)) (1--n) in
+  let xs = List.map ((o) string_of_num (element v)) (1--n) in
   "[" ^ end_itlist (fun s t -> s ^ ", " ^ t) xs ^
   (if n_raw > max_size then ", ...]" else "]");;
 
 let string_of_matrix max_size (m:matrix) =
   let i_raw,j_raw = dimensions m in
   let i = min max_size i_raw and j = min max_size j_raw in
-  let rstr = map (fun k -> string_of_vector j j (row k m)) (1--i) in
+  let rstr = List.map (fun k -> string_of_vector j j (row k m)) (1--i) in
   "["^end_itlist(fun s t -> s^";\n "^t) rstr ^
   (if j > max_size then "\n ...]" else "]");;
 
@@ -408,7 +407,7 @@ let rec poly_of_term t = match t with
 
 let sdpa_of_vector (v:vector) =
   let n = dim v in
-  let strs = map (o (decimalize 20)  (element v)) (1--n) in
+  let strs = List.map (o (decimalize 20)  (element v)) (1--n) in
   end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";;
 
 (* ------------------------------------------------------------------------- *)
@@ -445,15 +444,15 @@ let sdpa_of_matrix k (m:matrix) =
 (* ------------------------------------------------------------------------- *)
 
 let sdpa_of_problem comment obj mats =
-  let m = length mats - 1
-  and n,_ = dimensions (hd mats) in
+  let m = List.length mats - 1
+  and n,_ = dimensions (List.hd mats) in
   "\"" ^ comment ^ "\"\n" ^
   string_of_int m ^ "\n" ^
   "1\n" ^
   string_of_int n ^ "\n" ^
   sdpa_of_vector obj ^
   itlist2 (fun k m a -> sdpa_of_matrix (k - 1) m ^ a)
-          (1--length mats) mats "";;
+          (1--List.length mats) mats "";;
 
 (* ------------------------------------------------------------------------- *)
 (* More parser basics.                                                       *)
@@ -461,7 +460,7 @@ let sdpa_of_problem comment obj mats =
 
 let word s =
    end_itlist (fun p1 p2 -> (p1 ++ p2) >> (fun (s,t) -> s^t))
-              (map a (explode s));;
+              (List.map a (explode s));;
 let token s =
   many (some isspace) ++ word s ++ many (some isspace)
   >> (fun ((_,t),_) -> t);;
@@ -470,7 +469,7 @@ let decimal =
   let numeral = some isnum in
   let decimalint = atleast 1 numeral >> ((o) Num.num_of_string  implode) in
   let decimalfrac = atleast 1 numeral
-    >> (fun s -> Num.num_of_string(implode s) // pow10 (length s)) in
+    >> (fun s -> Num.num_of_string(implode s) // pow10 (List.length s)) in
   let decimalsig =
     decimalint ++ possibly (a "." ++ decimalfrac >> snd)
     >> (function (h,[x]) -> h +/ x | (h,_) -> h) in
@@ -626,13 +625,13 @@ let scale_then =
   fun solver obj mats ->
     let cd1 = itlist common_denominator mats (Int 1)
     and cd2 = common_denominator (snd obj)  (Int 1) in
-    let mats' = map (mapf (fun x -> cd1 */ x)) mats
+    let mats' = List.map (mapf (fun x -> cd1 */ x)) mats
     and obj' = vector_cmul cd2 obj in
     let max1 = itlist maximal_element mats' (Int 0)
     and max2 = maximal_element (snd obj') (Int 0) in
     let scal1 = pow2 (20-int_of_float(log(float_of_num max1) /. log 2.0))
     and scal2 = pow2 (20-int_of_float(log(float_of_num max2) /. log 2.0)) in
-    let mats'' = map (mapf (fun x -> x */ scal1)) mats'
+    let mats'' = List.map (mapf (fun x -> x */ scal1)) mats'
     and obj'' = vector_cmul scal2 obj' in
     solver obj'' mats'';;
 
@@ -651,7 +650,7 @@ let nice_vector n = mapa (nice_rational n);;
 
 let linear_program_basic a =
   let m,n = dimensions a in
-  let mats =  map (fun j -> diagonal (column j a)) (1--n)
+  let mats =  List.map (fun j -> diagonal (column j a)) (1--n)
   and obj = vector_const (Int 1) m in
   let rv,res = run_csdp false obj mats in
   if rv = 1 or rv = 2 then false
@@ -665,7 +664,7 @@ let linear_program_basic a =
 let linear_program a b =
   let m,n = dimensions a in
   if dim b <> m then failwith "linear_program: incompatible dimensions" else
-  let mats = diagonal b :: map (fun j -> diagonal (column j a)) (1--n)
+  let mats = diagonal b :: List.map (fun j -> diagonal (column j a)) (1--n)
   and obj = vector_const (Int 1) m in
   let rv,res = run_csdp false obj mats in
   if rv = 1 or rv = 2 then false
@@ -679,10 +678,10 @@ let linear_program a b =
 (* ------------------------------------------------------------------------- *)
 
 let in_convex_hull pts pt =
-  let pts1 = (1::pt) :: map (fun x -> 1::x) pts in
-  let pts2 = map (fun p -> map (fun x -> -x) p @ p) pts1 in
-  let n = length pts + 1
-  and v = 2 * (length pt + 1) in
+  let pts1 = (1::pt) :: List.map (fun x -> 1::x) pts in
+  let pts2 = List.map (fun p -> List.map (fun x -> -x) p @ p) pts1 in
+  let n = List.length pts + 1
+  and v = 2 * (List.length pt + 1) in
   let m = v + n - 1 in
   let mat =
     (m,n),
@@ -700,8 +699,8 @@ let minimal_convex_hull =
     | (m::ms) -> if in_convex_hull ms m then ms else ms@[m] in
   let augment m ms = funpow 3 augment1 (m::ms) in
   fun mons ->
-    let mons' = itlist augment (tl mons) [hd mons] in
-    funpow (length mons') augment1 mons';;
+    let mons' = itlist augment (List.tl mons) [List.hd mons] in
+    funpow (List.length mons') augment1 mons';;
 
 (* ------------------------------------------------------------------------- *)
 (* Stuff for "equations" (generic A->num functions).                         *)
@@ -743,7 +742,7 @@ let eliminate_equations =
                   let b = tryapplyd e v (Int 0) in
                   if b =/ Int 0 then e else
                   equation_add e (equation_cmul (minus_num b // a) eq) in
-                eliminate vs ((v |-> eq') (mapf elim dun)) (map elim oeqs)
+                eliminate vs ((v |-> eq') (mapf elim dun)) (List.map elim oeqs)
             with Failure _ -> eliminate vs dun eqs in
   fun one vars eqs ->
     let assig = eliminate vars undefined eqs in
@@ -774,7 +773,7 @@ let eliminate_all_equations one =
           let b = tryapplyd e v (Int 0) in
           if b =/ Int 0 then e else
           equation_add e (equation_cmul (minus_num b // a) eq) in
-        eliminate ((v |-> eq') (mapf elim dun)) (map elim oeqs) in
+        eliminate ((v |-> eq') (mapf elim dun)) (List.map elim oeqs) in
   fun eqs ->
     let assig = eliminate undefined eqs in
     let vs = foldl (fun a x f -> subtract (dom f) [one] @ a) [] assig in
@@ -805,14 +804,14 @@ let solve_equations one eqs =
 
 let newton_polytope pol =
   let vars = poly_variables pol in
-  let mons = map (fun m -> map (fun x -> monomial_degree x m) vars) (dom pol)
-  and ds = map (fun x -> (degree x pol + 1) / 2) vars in
+  let mons = List.map (fun m -> List.map (fun x -> monomial_degree x m) vars) (dom pol)
+  and ds = List.map (fun x -> (degree x pol + 1) / 2) vars in
   let all = itlist (fun n -> allpairs (fun h t -> h::t) (0--n)) ds [[]]
   and mons' = minimal_convex_hull mons in
   let all' =
-    filter (fun m -> in_convex_hull mons' (map (fun x -> 2 * x) m)) all in
-  map (fun m -> itlist2 (fun v i a -> if i = 0 then a else (v |-> i) a)
-                        vars m monomial_1) (rev all');;
+    List.filter (fun m -> in_convex_hull mons' (List.map (fun x -> 2 * x) m)) all in
+  List.map (fun m -> itlist2 (fun v i a -> if i = 0 then a else (v |-> i) a)
+                        vars m monomial_1) (List.rev all');;
 
 (* ------------------------------------------------------------------------- *)
 (* Diagonalize (Cholesky/LDU) the matrix corresponding to a quadratic form.  *)
@@ -851,10 +850,10 @@ let deration d =
     let a = foldl (fun a i c -> lcm_num a (denominator c)) (Int 1) (snd l) //
             foldl (fun a i c -> gcd_num a (numerator c)) (Int 0) (snd l) in
     (c // (a */ a)),mapa (fun x -> a */ x) l in
-  let d' = map adj d in
+  let d' = List.map adj d in
   let a = itlist ((o) lcm_num ( (o) denominator fst)) d' (Int 1) //
           itlist ((o) gcd_num ( (o) numerator fst)) d' (Int 0)  in
-  (Int 1 // a),map (fun (c,l) -> (a */ c,l)) d';;
+  (Int 1 // a),List.map (fun (c,l) -> (a */ c,l)) d';;
 
 (* ------------------------------------------------------------------------- *)
 (* Enumeration of monomials with given multidegree bound.                    *)
@@ -865,8 +864,8 @@ let rec enumerate_monomials d vars =
   else if d = 0 then [undefined]
   else if vars = [] then [monomial_1] else
   let alts =
-    map (fun k -> let oths = enumerate_monomials (d - k) (tl vars) in
-                  map (fun ks -> if k = 0 then ks else (hd vars |-> k) ks) oths)
+    List.map (fun k -> let oths = enumerate_monomials (d - k) (List.tl vars) in
+                  List.map (fun ks -> if k = 0 then ks else (List.hd vars |-> k) ks) oths)
         (0--d) in
   end_itlist (@) alts;;
 
@@ -883,7 +882,7 @@ let rec enumerate_products d pols =
   | (p,b)::ps -> let e = multidegree p in
                  if e = 0 then enumerate_products d ps else
                  enumerate_products d ps @
-                 map (fun (q,c) -> poly_mul p q,Product(b,c))
+                 List.map (fun (q,c) -> poly_mul p q,Product(b,c))
                      (enumerate_products (d - e) ps);;
 
 (* ------------------------------------------------------------------------- *)
@@ -936,15 +935,15 @@ let sdpa_of_blockdiagonal k m =
 (* ------------------------------------------------------------------------- *)
 
 let sdpa_of_blockproblem comment nblocks blocksizes obj mats =
-  let m = length mats - 1 in
+  let m = List.length mats - 1 in
   "\"" ^ comment ^ "\"\n" ^
   string_of_int m ^ "\n" ^
   string_of_int nblocks ^ "\n" ^
-  (end_itlist (fun s t -> s^" "^t) (map string_of_int blocksizes)) ^
+  (end_itlist (fun s t -> s^" "^t) (List.map string_of_int blocksizes)) ^
   "\n" ^
   sdpa_of_vector obj ^
   itlist2 (fun k m a -> sdpa_of_blockdiagonal (k - 1) m ^ a)
-          (1--length mats) mats "";;
+          (1--List.length mats) mats "";;
 
 (* ------------------------------------------------------------------------- *)
 (* Hence run CSDP on a problem in block diagonal form.                       *)
@@ -996,35 +995,35 @@ let bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);;
 (* ------------------------------------------------------------------------- *)
 
 let blocks blocksizes bm =
-  map (fun (bs,b0) ->
+  List.map (fun (bs,b0) ->
         let m = foldl
           (fun a (b,i,j) c -> if b = b0 then ((i,j) |-> c) a else a)
           undefined bm in
         (((bs,bs),m):matrix))
-      (zip blocksizes (1--length blocksizes));;
+      (zip blocksizes (1--List.length blocksizes));;
 
 (* ------------------------------------------------------------------------- *)
 (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
 (* ------------------------------------------------------------------------- *)
 
 let real_positivnullstellensatz_general linf d eqs leqs pol =
-  let vars = itlist ((o) union poly_variables) (pol::eqs @ map fst leqs) [] in
+  let vars = itlist ((o) union poly_variables) (pol::eqs @ List.map fst leqs) [] in
   let monoid =
     if linf then
       (poly_const num_1,Rational_lt num_1)::
-      (filter (fun (p,c) -> multidegree p <= d) leqs)
+      (List.filter (fun (p,c) -> multidegree p <= d) leqs)
     else enumerate_products d leqs in
-  let nblocks = length monoid in
+  let nblocks = List.length monoid in
   let mk_idmultiplier k p =
     let e = d - multidegree p in
     let mons = enumerate_monomials e vars in
-    let nons = zip mons (1--length mons) in
+    let nons = zip mons (1--List.length mons) in
     mons,
     itlist (fun (m,n) -> (m |-> ((-k,-n,n) |=> Int 1))) nons undefined in
   let mk_sqmultiplier k (p,c) =
     let e = (d - multidegree p) / 2 in
     let mons = enumerate_monomials e vars in
-    let nons = zip mons (1--length mons) in
+    let nons = zip mons (1--List.length mons) in
     mons,
     itlist (fun (m1,n1) ->
       itlist (fun (m2,n2) a ->
@@ -1035,9 +1034,9 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
           (m |-> equation_add ((k,n1,n2) |=> c) e) a)
          nons)
        nons undefined in
-  let sqmonlist,sqs = unzip(map2 mk_sqmultiplier (1--length monoid) monoid)
-  and idmonlist,ids =  unzip(map2 mk_idmultiplier (1--length eqs) eqs) in
-  let blocksizes = map length sqmonlist in
+  let sqmonlist,sqs = unzip(List.map2 mk_sqmultiplier (1--List.length monoid) monoid)
+  and idmonlist,ids =  unzip(List.map2 mk_idmultiplier (1--List.length eqs) eqs) in
+  let blocksizes = List.map List.length sqmonlist in
   let bigsum =
     itlist2 (fun p q a -> epoly_pmul p q a) eqs ids
             (itlist2 (fun (p,c) s a -> epoly_pmul p s a) monoid sqs
@@ -1055,8 +1054,8 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
   let diagents = foldl
     (fun a (b,i,j) e -> if b > 0 & i = j then equation_add e a else a)
     undefined allassig in
-  let mats = map mk_matrix qvars
-  and obj = length pvs,
+  let mats = List.map mk_matrix qvars
+  and obj = List.length pvs,
             itern 1 pvs (fun v i -> (i |--> tryapplyd diagents v (Int 0)))
                         undefined in
   let raw_vec = if pvs = [] then vector_0 0
@@ -1071,11 +1070,11 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
      (fun i a -> bmatrix_add (bmatrix_cmul (element vec i) (el i mats)) a)
      (bmatrix_neg (el 0 mats)) in
     let allmats = blocks blocksizes blockmat in
-    vec,map diag allmats in
+    vec,List.map diag allmats in
   let vec,ratdias =
     if pvs = [] then find_rounding num_1
-    else tryfind find_rounding (map Num.num_of_int (1--31) @
-                                map pow2 (5--66)) in
+    else tryfind find_rounding (List.map Num.num_of_int (1--31) @
+                                List.map pow2 (5--66)) in
   let newassigs =
     itlist (fun k -> el (k - 1) pvs |-> element vec k)
            (1--dim vec) ((0,0,0) |=> Int(-1)) in
@@ -1088,11 +1087,11 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
   let mk_sos mons =
     let mk_sq (c,m) =
         c,itlist (fun k a -> (el (k - 1) mons |--> element m k) a)
-                 (1--length mons) undefined in
-    map mk_sq in
-  let sqs = map2 mk_sos sqmonlist ratdias
-  and cfs = map poly_of_epoly ids in
-  let msq = filter (fun (a,b) -> b <> []) (map2 (fun a b -> a,b) monoid sqs) in
+                 (1--List.length mons) undefined in
+    List.map mk_sq in
+  let sqs = List.map2 mk_sos sqmonlist ratdias
+  and cfs = List.map poly_of_epoly ids in
+  let msq = List.filter (fun (a,b) -> b <> []) (List.map2 (fun a b -> a,b) monoid sqs) in
   let eval_sq sqs = itlist
    (fun (c,q) -> poly_add (poly_cmul c (poly_mul q q))) sqs poly_0 in
   let sanity =
@@ -1100,7 +1099,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
            (itlist2 (fun p q -> poly_add (poly_mul p q)) cfs eqs
                     (poly_neg pol)) in
   if not(is_undefined sanity) then raise Sanity else
-  cfs,map (fun (a,b) -> snd a,b) msq;;
+  cfs,List.map (fun (a,b) -> snd a,b) msq;;
 
 (* ------------------------------------------------------------------------- *)
 (* Iterative deepening.                                                      *)
@@ -1138,7 +1137,7 @@ let monomial_order =
     else lexorder mon1 mon2;;
 
 let dest_poly p =
-  map (fun (m,c) -> c,dest_monomial m)
+  List.map (fun (m,c) -> c,dest_monomial m)
       (sort (fun (m1,_) (m2,_) -> monomial_order m1 m2) (graph p));;
 
 (* ------------------------------------------------------------------------- *)
@@ -1164,7 +1163,7 @@ let term_of_cmonomial =
 let term_of_poly =
   fun p ->
     if p = poly_0 then Zero else
-    let cms = map term_of_cmonomial
+    let cms = List.map term_of_cmonomial
      (sort (fun (m1,_) (m2,_) -> monomial_order m1 m2) (graph p)) in
     end_itlist (fun t1 t2 -> Add (t1,t2)) cms;;
 
@@ -1173,7 +1172,7 @@ let term_of_sqterm (c,p) =
 
 let term_of_sos (pr,sqs) =
   if sqs = [] then pr
-  else Product(pr,end_itlist (fun a b -> Sum(a,b)) (map term_of_sqterm sqs));;
+  else Product(pr,end_itlist (fun a b -> Sum(a,b)) (List.map term_of_sqterm sqs));;
 
 (* ------------------------------------------------------------------------- *)
 (* Interface to HOL.                                                         *)
@@ -1371,14 +1370,14 @@ let SOS_RULE tm =
 
 let rec allpermutations l =
   if l = [] then [[]] else
-  itlist (fun h acc -> map (fun t -> h::t)
+  itlist (fun h acc -> List.map (fun t -> h::t)
                 (allpermutations (subtract l [h])) @ acc) l [];;
 
 let allvarorders l =
-  map (fun vlis x -> index x vlis) (allpermutations l);;
+  List.map (fun vlis x -> index x vlis) (allpermutations l);;
 
 let changevariables_monomial zoln (m:monomial) =
-  foldl (fun a x k -> (assoc x zoln |-> k) a) monomial_1 m;;
+  foldl (fun a x k -> (List.assoc x zoln |-> k) a) monomial_1 m;;
 
 let changevariables zoln pol =
   foldl (fun a m c -> (changevariables_monomial zoln m |-> c) a)
@@ -1390,7 +1389,7 @@ let changevariables zoln pol =
 
 let sdpa_of_vector (v:vector) =
   let n = dim v in
-  let strs = map (o (decimalize 20) (element v)) (1--n) in
+  let strs = List.map (o (decimalize 20) (element v)) (1--n) in
   end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";;
 
 let sdpa_of_blockdiagonal k m =
@@ -1412,15 +1411,15 @@ let sdpa_of_matrix k (m:matrix) =
      " " ^ decimalize 20 c ^ "\n" ^ a) mss "";;
 
 let sdpa_of_problem comment obj mats =
-  let m = length mats - 1
-  and n,_ = dimensions (hd mats) in
+  let m = List.length mats - 1
+  and n,_ = dimensions (List.hd mats) in
   "\"" ^ comment ^ "\"\n" ^
   string_of_int m ^ "\n" ^
   "1\n" ^
   string_of_int n ^ "\n" ^
   sdpa_of_vector obj ^
   itlist2 (fun k m a -> sdpa_of_matrix (k - 1) m ^ a)
-          (1--length mats) mats "";;
+          (1--List.length mats) mats "";;
 
 let run_csdp dbg obj mats =
   let input_file = Filename.temp_file "sos" ".dat-s" in
@@ -1455,33 +1454,33 @@ let csdp obj mats =
 let sumofsquares_general_symmetry tool pol =
   let vars = poly_variables pol
   and lpps = newton_polytope pol in
-  let n = length lpps in
+  let n = List.length lpps in
   let sym_eqs =
-    let invariants = filter
+    let invariants = List.filter
      (fun vars' ->
         is_undefined(poly_sub pol (changevariables (zip vars vars') pol)))
      (allpermutations vars) in
-    let lpns = zip lpps (1--length lpps) in
+    let lpns = zip lpps (1--List.length lpps) in
     let lppcs =
-      filter (fun (m,(n1,n2)) -> n1 <= n2)
+      List.filter (fun (m,(n1,n2)) -> n1 <= n2)
              (allpairs
                (fun (m1,n1) (m2,n2) -> (m1,m2),(n1,n2)) lpns lpns) in
     let clppcs = end_itlist (@)
-       (map (fun ((m1,m2),(n1,n2)) ->
-                map (fun vars' ->
+       (List.map (fun ((m1,m2),(n1,n2)) ->
+                List.map (fun vars' ->
                         (changevariables_monomial (zip vars vars') m1,
                          changevariables_monomial (zip vars vars') m2),(n1,n2))
                     invariants)
             lppcs) in
-    let clppcs_dom = setify(map fst clppcs) in
-    let clppcs_cls = map (fun d -> filter (fun (e,_) -> e = d) clppcs)
+    let clppcs_dom = setify(List.map fst clppcs) in
+    let clppcs_cls = List.map (fun d -> List.filter (fun (e,_) -> e = d) clppcs)
                          clppcs_dom in
-    let eqvcls = map (o setify (map snd)) clppcs_cls in
+    let eqvcls = List.map (o setify (List.map snd)) clppcs_cls in
     let mk_eq cls acc =
       match cls with
         [] -> raise Sanity
       | [h] -> acc
-      | h::t -> map (fun k -> (k |-> Int(-1)) (h |=> Int 1)) t @ acc in
+      | h::t -> List.map (fun k -> (k |-> Int(-1)) (h |=> Int 1)) t @ acc in
     itlist mk_eq eqvcls [] in
   let eqs = foldl (fun a x y -> y::a) []
    (itern 1 lpps (fun m1 n1 ->
@@ -1497,15 +1496,15 @@ let sumofsquares_general_symmetry tool pol =
   let allassig = itlist (fun v -> (v |-> (v |=> Int 1))) pvs assig in
   let qvars = (0,0)::pvs in
   let diagents =
-    end_itlist equation_add (map (fun i -> apply allassig (i,i)) (1--n)) in
+    end_itlist equation_add (List.map (fun i -> apply allassig (i,i)) (1--n)) in
   let mk_matrix v =
    ((n,n),
     foldl (fun m (i,j) ass -> let c = tryapplyd ass v (Int 0) in
                               if c =/ Int 0 then m else
                               ((j,i) |-> c) (((i,j) |-> c) m))
           undefined allassig :matrix) in
-  let mats = map mk_matrix qvars
-  and obj = length pvs,
+  let mats = List.map mk_matrix qvars
+  and obj = List.length pvs,
             itern 1 pvs (fun v i -> (i |--> tryapplyd diagents v (Int 0)))
                 undefined in
   let raw_vec = if pvs = [] then vector_0 0 else tool obj mats in
@@ -1524,12 +1523,12 @@ let sumofsquares_general_symmetry tool pol =
        let mat = matrix_neg (el 0 mats) in
        deration(diag mat)
     else
-       tryfind find_rounding (map Num.num_of_int (1--31) @
-                              map pow2 (5--66)) in
+       tryfind find_rounding (List.map Num.num_of_int (1--31) @
+                              List.map pow2 (5--66)) in
   let poly_of_lin(d,v) =
     d,foldl(fun a i c -> (el (i - 1) lpps |-> c) a) undefined (snd v) in
-  let lins = map poly_of_lin dia in
-  let sqs = map (fun (d,l) -> poly_mul (poly_const d) (poly_pow l 2)) lins in
+  let lins = List.map poly_of_lin dia in
+  let sqs = List.map (fun (d,l) -> poly_mul (poly_const d) (poly_pow l 2)) lins in
   let sos = poly_cmul rat (end_itlist poly_add sqs) in
   if is_undefined(poly_sub sos pol) then rat,lins else raise Sanity;;
 
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index baf90d4da..e592611ac 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -8,7 +8,6 @@
 (* ========================================================================= *)
 open Sos_types
 open Num
-open List
 
 let debugging = ref false;;
 
@@ -62,7 +61,7 @@ let lcm_num x y =
 (* ------------------------------------------------------------------------- *)
 
 let rec el n l =
-  if n = 0 then hd l else el (n - 1) (tl l);;
+  if n = 0 then List.hd l else el (n - 1) (List.tl l);;
 
 
 (* ------------------------------------------------------------------------- *)
@@ -169,7 +168,7 @@ let insert x l =
 
 let union l1 l2 = itlist insert l1 l2;;
 
-let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1;;
+let subtract l1 l2 = List.filter (fun x -> not (mem x l2)) l1;;
 
 (* ------------------------------------------------------------------------- *)
 (* Merging and bottom-up mergesort.                                          *)
@@ -224,7 +223,7 @@ let rec sort cmp lis =
   match lis with
     [] -> []
   | piv::rest ->
-      let r,l = partition (cmp piv) rest in
+      let r,l = List.partition (cmp piv) rest in
       (sort cmp l) @ (piv::(sort cmp r));;
 
 (* ------------------------------------------------------------------------- *)
@@ -416,7 +415,7 @@ let (|=>) = fun x y -> (x |-> y) undefined;;
 let rec choose t =
   match t with
     Empty -> failwith "choose: completely undefined function"
-  | Leaf(h,l) -> hd l
+  | Leaf(h,l) -> List.hd l
   | Branch(b,p,t1,t2) -> choose t1;;
 
 (* ------------------------------------------------------------------------- *)
@@ -583,7 +582,7 @@ let strings_of_file filename =
   let rec suck_lines acc =
     try let l = Pervasives.input_line fd in
         suck_lines (l::acc)
-    with End_of_file -> rev acc in
+    with End_of_file -> List.rev acc in
   let data = suck_lines [] in
   (Pervasives.close_in fd; data);;
 
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index b635fd1fc..55980b330 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -16,7 +16,6 @@ a polynomial is a sorted list of (coefficient, monomial)
  *)
 
 open Utile
-open List
 
 exception NotInIdeal
 
@@ -219,9 +218,9 @@ let equal =
     (fun (c1,m1) (c2,m2) -> P.equal c1 c2 && m1=m2)
 
 let hash p =
-  let c = map fst p in
-  let m = map snd p in
-  fold_left (fun h p -> h * 17 + P.hash p) (Hashtbl.hash m) c
+  let c = List.map fst p in
+  let m = List.map snd p in
+  List.fold_left (fun h p -> h * 17 + P.hash p) (Hashtbl.hash m) c
 
 module Hashpol = Hashtbl.Make(
   struct
@@ -236,8 +235,8 @@ module Hashpol = Hashtbl.Make(
 open Format
 
 let getvar lv i =
-  try (nth lv i)
-  with _ -> (fold_left (fun r x -> r^" "^x) "lv= " lv)
+  try (List.nth lv i)
+  with _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv)
     ^" i="^(string_of_int i)
 
 let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
@@ -362,8 +361,8 @@ let stringPcut p =
   (*Polynomesrec.nsP1:=20;*)
   nsP2:=10;
   let res =
-    if (length p)> !nsP2
-    then (stringP [hd p])^" + "^(string_of_int (length p))^" terms"
+    if (List.length p)> !nsP2
+    then (stringP [List.hd p])^" + "^(string_of_int (List.length p))^" terms"
     else  stringP p in
   (*Polynomesrec.nsP1:= max_int;*)
   nsP2:= max_int;
@@ -462,7 +461,7 @@ let puisP p n=
   match p with
     [] -> []
   |_ ->
-      let d = nvar (snd (hd p)) in
+      let d = nvar (snd (List.hd p)) in
       let rec puisP n =
 	match n with
 	  0 -> [coef1, Array.create (d+1) 0]
@@ -483,7 +482,7 @@ let contentPlist lp =
   match lp with
   |[] -> coef1
   |p::l1 ->
-      fold_left
+      List.fold_left
 	(fun r q ->
 	  if P.equal r coef1 || P.equal r coefm1
 	  then r
@@ -500,7 +499,7 @@ let polynom0 =  {pol = ref []; num = 0; sugar = 0}
    
 let ppol p = !(p.pol)
 
-let lm p = snd (hd (ppol p))
+let lm p = snd (List.hd (ppol p))
 
 let nallpol = ref 0
 
@@ -520,7 +519,7 @@ let new_allpol p s =
 let rec selectdiv m l =
   match l with
     [] -> polynom0
-  |q::r -> let m'= snd (hd (ppol q)) in
+  |q::r -> let m'= snd (List.hd (ppol q)) in
     match (div_mon_test m m') with
       true -> q
     |false -> selectdiv m r
@@ -549,7 +548,7 @@ let div_coef a b = P.divP a b
 (* remainder r of the division of p by polynomials of l, returns (c,r) where c is the coefficient for pseudo-division : c p = sum_i q_i p_i + r *)
 
 let reduce2 p l =
-  let l = if nouveaux_pol_en_tete then rev l else l in
+  let l = if nouveaux_pol_en_tete then List.rev l else l in
   let rec reduce p =
     match p with
       [] -> (coef1,[])
@@ -600,8 +599,8 @@ let coefpoldep_set p q c =
 
 let initcoefpoldep d lp =
   poldep:=lp;
-  poldepcontent:= map (fun p -> contentP (ppol p)) lp;
-  iter
+  poldepcontent:= List.map (fun p -> contentP (ppol p)) lp;
+  List.iter
     (fun p -> coefpoldep_set p p (polconst d (coef_of_int 1)))
     lp
 
@@ -609,7 +608,7 @@ let initcoefpoldep d lp =
    divides without pseudodivisions *)
 
 let reduce2_trace p l lcp =
-  let l = if nouveaux_pol_en_tete then rev l else l in
+  let l = if nouveaux_pol_en_tete then List.rev l else l in
   (* rend (lq,r), ou r = p + sum(lq) *)
   let rec reduce p =
     match p with
@@ -645,10 +644,10 @@ let reduce2_trace p l lcp =
      info ((stringP x)^"\n"))
      lq;
      info "ok\n";*)
-  (map2
+  (List.map2
      (fun c0 q ->
        let c =
-	 fold_left
+	 List.fold_left
 	   (fun x (a,m,s) ->
 	     if equal (ppol s) (ppol q)
 	     then
@@ -671,7 +670,7 @@ let pol_courant = ref polynom0
 let sugar_flag = ref true
 
 let compute_sugar p =
-  fold_left (fun s (a,m) -> max s m.(0)) 0 p
+  List.fold_left (fun s (a,m) -> max s m.(0)) 0 p
 
 let mk_polynom p = 
   new_allpol p (compute_sugar p)
@@ -679,12 +678,12 @@ let mk_polynom p =
 let spol ps qs=
   let p = ppol ps in
   let q = ppol qs in
-  let m = snd (hd p) in
-  let m'= snd (hd q) in
-  let a = fst (hd p) in
-  let b = fst (hd q) in
-  let p'= tl p in
-  let q'= tl q in
+  let m = snd (List.hd p) in
+  let m'= snd (List.hd q) in
+  let a = fst (List.hd p) in
+  let b = fst (List.hd q) in
+  let p'= List.tl p in
+  let q'= List.tl q in
   let c = (pgcdpos a b) in
   let m''=(ppcm_mon m m') in
   let m1 = div_mon m'' m in
@@ -708,8 +707,8 @@ let spol ps qs=
   
 
 let etrangers p p'=
-  let m = snd (hd p) in
-  let m'= snd (hd p') in
+  let m = snd (List.hd p) in
+  let m'= snd (List.hd p') in
   let d = nvar m in
   let res=ref true in
   let i=ref 1 in
@@ -722,9 +721,9 @@ let etrangers p p'=
 (* teste if head monomial of p'' divides lcm of lhead monomials of p and p' *)
 
 let div_ppcm p p' p'' =
-  let m = snd (hd p) in
-  let m'= snd (hd p') in
-  let m''= snd (hd p'') in
+  let m = snd (List.hd p) in
+  let m'= snd (List.hd p') in
+  let m''= snd (List.hd p'') in
   let d = nvar m in
   let res=ref true in
   let i=ref 1 in
@@ -822,10 +821,10 @@ let ordcpair ((i1,j1),m1) ((i2,j2),m2) =
   compare_mon m1 m2 
 
 let sortcpairs lcp = 
-  sort ordcpair lcp
+  List.sort ordcpair lcp
 
 let mergecpairs l1 l2 =
-  merge ordcpair l1 l2 
+  List.merge ordcpair l1 l2 
 
 let ord i j =
   if i<j then (i,j) else (j,i)
@@ -837,7 +836,7 @@ let cpair p q =
 	 ppcm_mon (lm p) (lm q))]
       
 let cpairs1 p lq =
-  sortcpairs (fold_left (fun r q -> r @ (cpair p q)) [] lq)
+  sortcpairs (List.fold_left (fun r q -> r @ (cpair p q)) [] lq)
     
 let cpairs lp =
   let rec aux l =
@@ -848,18 +847,18 @@ let cpairs lp =
     
     
 let critere2 ((i,j),m) lp lcp =
-  exists
+  List.exists
     (fun h ->
       h.num <> i && h.num <> j
         && (div_mon_test m (lm h))
 	&& (let c1 = ord i h.num in
-	not (exists (fun (c,_) -> c1 = c) lcp))
+	not (List.exists (fun (c,_) -> c1 = c) lcp))
 	&& (let c1 = ord j h.num in
-	not (exists (fun (c,_) -> c1 = c) lcp)))
+	not (List.exists (fun (c,_) -> c1 = c) lcp)))
     lp
 
 let critere3 ((i,j),m) lp lcp =
-  exists
+  List.exists
     (fun h ->
       h.num <> i && h.num <> j
         && (div_mon_test m (lm h))
@@ -880,8 +879,8 @@ let step = ref 0
 
 let infobuch p q =
   if !step = 0 
-  then (info ("[" ^ (string_of_int (length p))
-              ^ "," ^  (string_of_int (length q))
+  then (info ("[" ^ (string_of_int (List.length p))
+              ^ "," ^  (string_of_int (List.length q))
               ^ "]"))
 
 (* in lp new polynomials are at the end *)
@@ -899,13 +898,13 @@ let test_dans_ideal p lp lp0 =
   pol_courant:= mk_polynom r;
   if r=[]
   then (info "polynomial reduced to 0\n";
-	let lcp = map (fun q -> []) !poldep in
+	let lcp = List.map (fun q -> []) !poldep in
 	let c = !coef_courant in
 	let (lcq,r) = reduce2_trace (emultP c p) lp lcp in
 	info "r ok\n";
 	info ("r: "^(stringP r)^"\n");
         let res=ref  (emultP c p) in
-	iter2
+	List.iter2
 	  (fun cq q -> res:=plusP (!res) (multP cq (ppol q));
 	  )
 	  lcq !poldep;
@@ -915,22 +914,22 @@ let test_dans_ideal p lp lp0 =
 	  match lp with
 	  |[] -> []
 	  |p::lp ->
-	      (map
+	      (List.map
 		 (fun q -> coefpoldep_find p q)
 		 lp)::(aux lp)
 	in
 	let coefficient_multiplicateur = c in
-	let liste_polynomes_de_depart = rev lp0 in
+	let liste_polynomes_de_depart = List.rev lp0 in
 	let polynome_a_tester = p in
 	let liste_des_coefficients_intermediaires =
-	  (let lci = rev (aux (rev lp)) in
+	  (let lci = List.rev (aux (List.rev lp)) in
 	  let lci = ref lci (* (map rev lci) *) in
-	  iter (fun x -> lci := tl (!lci)) lp0;
+	  List.iter (fun x -> lci := List.tl (!lci)) lp0;
 	  !lci) in
 	let liste_des_coefficients =
-	  map
+	  List.map
 	    (fun cq -> emultP (coef_of_int (-1)) cq)
-	    (rev lcq) in
+	    (List.rev lcq) in
 	(liste_polynomes_de_depart,
 	 polynome_a_tester,
 	 {coef = coefficient_multiplicateur;
@@ -945,7 +944,7 @@ let test_dans_ideal p lp lp0 =
 let divide_rem_with_critical_pair = ref false
 
 let list_diff l x =
-  filter (fun y -> y <> x) l
+  List.filter (fun y -> y <> x) l
 
 let deg_hom p =
   match p with
@@ -983,12 +982,12 @@ let pbuchf pq p lp0=
 (*		info "pair reduced\n";*)
 		  a.pol := emultP ca (ppol a);
 		  let (lca,a0) = reduce2_trace (ppol a) lp
-		      (map (fun q -> emultP ca (coefpoldep_find a q))
+		      (List.map (fun q -> emultP ca (coefpoldep_find a q))
 			 !poldep) in
 (*		info "paire re-reduced";*)
 		  a.pol := a0;
 (*		  let a0 = new_allpol a0 sa in*)
-		  iter2 (fun c q ->
+		  List.iter2 (fun c q ->
 		    coefpoldep_remove a q;
 		    coefpoldep_set a q c) lca !poldep;
 		  let a0 = a in
@@ -1008,7 +1007,7 @@ let is_homogeneous p =
   match p with
   | [] -> true
   | (a,m)::p1 -> let d = m.(0) in
-    for_all (fun (b,m') -> m'.(0)=d) p1
+    List.for_all (fun (b,m') -> m'.(0)=d) p1
     
 (* returns
    c
@@ -1030,14 +1029,14 @@ let in_ideal d lp p =
   Hashtbl.clear coefpoldep;
   nallpol := 0;
   allpol := Array.create 1000 polynom0;
-  homogeneous := for_all is_homogeneous (p::lp);
+  homogeneous := List.for_all is_homogeneous (p::lp);
   if !homogeneous then info "homogeneous polynomials\n";
   info ("p: "^(stringPcut p)^"\n");
-  info ("lp:\n"^(fold_left (fun r p -> r^(stringPcut p)^"\n") "" lp));
+  info ("lp:\n"^(List.fold_left (fun r p -> r^(stringPcut p)^"\n") "" lp));
   (*info ("p: "^(stringP p)^"\n");
   info ("lp:\n"^(fold_left (fun r p -> r^(stringP p)^"\n") "" lp));*)
 
-  let lp = map mk_polynom lp in
+  let lp = List.map mk_polynom lp in
   let p = mk_polynom p in
   initcoefpoldep d lp;
   coef_courant:=coef1;
@@ -1048,7 +1047,7 @@ let in_ideal d lp p =
     with NotInIdeal -> pbuchf (lp, (cpairs lp)) p lp in
   info "computed\n";
 
-  (map ppol lp1, p1, cert)
+  (List.map ppol lp1, p1, cert)
     
 (* *)
 end
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a494e2f93..254adb5f6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -37,7 +37,6 @@ open Libnames
 open Globnames
 open Nameops
 open Classops
-open List
 open Recordops
 open Evarutil
 open Pretype_errors
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 0d6bc39f3..4711d9f6d 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -25,7 +25,6 @@ open Term
 open Sign
 open Names
 open Evd
-open List
 open Pp
 open Errors
 open Util
@@ -149,7 +148,7 @@ let etype_of_evar evs hyps concl =
     | [] ->
 	let t', s, trans = subst_evar_constr evs n mkVar concl in
 	  subst_vars acc 0 t', s, trans
-  in aux [] 0 (rev hyps)
+  in aux [] 0 (List.rev hyps)
 
 
 open Tacticals
@@ -240,7 +239,7 @@ let eterm_obligations env name evm fs ?status t ty =
   in
   let evts =
     (* Remove existential variables in types and build the corresponding products *)
-    fold_right
+    List.fold_right
       (fun (id, (n, nstr), ev) l ->
 	 let hyps = Evd.evar_filtered_context ev in
 	 let hyps = trunc_named_context nc_len hyps in