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

1 files changed, 54 insertions, 55 deletions

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