From 826eb7c6d11007dfd747d49852e71a22e0a3850a Mon Sep 17 00:00:00 2001 From: xclerc Date: Thu, 19 Sep 2013 12:59:04 +0000 Subject: Get rid of the uses of deprecated OCaml elements (still remaining compatible with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/mlutil.ml | 2 +- plugins/fourier/fourierR.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 6 +++--- plugins/micromega/polynomial.ml | 2 +- plugins/nsatz/ideal.ml | 18 +++++++++--------- plugins/nsatz/utile.ml | 2 +- plugins/omega/coq_omega.ml | 2 +- plugins/omega/omega.ml | 14 +++++++------- plugins/quote/quote.ml | 8 ++++---- plugins/romega/const_omega.ml | 2 +- plugins/syntax/ascii_syntax.ml | 2 +- plugins/syntax/r_syntax.ml | 8 ++++---- 12 files changed, 34 insertions(+), 34 deletions(-) (limited to 'plugins') diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 0903f85a0..4ad681c05 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1248,7 +1248,7 @@ let rec non_stricts add cand = function let n = List.length i in let cand = lift n cand in let cand = pop n (non_stricts add cand t) in - Sort.merge (<=) cand c) [] v + List.merge Pervasives.compare cand c) [] v (* [merge] may duplicates some indices, but I don't mind. *) | MLmagic t -> non_stricts add cand t diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 02503ab47..3dd384ee8 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -271,7 +271,7 @@ let fourier_lineq lineq1 = f.hflin.fhom) lineq1; let sys= List.map (fun h-> - let v=Array.create ((!nvar)+1) r0 in + let v=Array.make ((!nvar)+1) r0 in Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c) h.hflin.fhom; ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 15e284398..356853573 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -916,9 +916,9 @@ let generalize_non_dep hyp g = let to_revert,_ = Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> if List.mem hyp hyps - or List.exists (Termops.occur_var_in_decl env hyp) keep - or Termops.occur_var env hyp hyp_typ - or Termops.is_section_variable hyp (* should be dangerous *) + || List.exists (Termops.occur_var_in_decl env hyp) keep + || Termops.occur_var env hyp hyp_typ + || Termops.is_section_variable hyp (* should be dangerous *) then (clear,decl::keep) else (hyp::clear,keep)) ~init:([],[]) (pf_env g) diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index 339e10661..f993dc14f 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -218,7 +218,7 @@ struct let fold = P.fold - let is_null p = fold (fun mn vl b -> b & sign_num vl = 0) p true + let is_null p = fold (fun mn vl b -> b && sign_num vl = 0) p true let compare = compare compare_num diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 5ad546588..6beb96c38 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -133,7 +133,7 @@ let deg m = m.(0) let mult_mon m m' = let d = nvar m in - let m'' = Array.create (d+1) 0 in + let m'' = Array.make (d+1) 0 in for i=0 to d do m''.(i)<- (m.(i)+m'.(i)); done; @@ -167,7 +167,7 @@ let compare_mon m m' = let div_mon m m' = let d = nvar m in - let m'' = Array.create (d+1) 0 in + let m'' = Array.make (d+1) 0 in for i=0 to d do m''.(i)<- (m.(i)-m'.(i)); done; @@ -198,7 +198,7 @@ let set_deg m = (* lcm *) let ppcm_mon m m' = let d = nvar m in - let m'' = Array.create (d+1) 0 in + let m'' = Array.make (d+1) 0 in for i=1 to d do m''.(i)<- (max m.(i) m'.(i)); done; @@ -397,7 +397,7 @@ let zeroP = [] (* returns a constant polynom ial with d variables *) let polconst d c = - let m = Array.create (d+1) 0 in + let m = Array.make (d+1) 0 in let m = set_deg m in [(c,m)] @@ -430,7 +430,7 @@ let coef_of_int x = P.of_num (Num.Int x) (* variable i *) let gen d i = - let m = Array.create (d+1) 0 in + let m = Array.make (d+1) 0 in m.(i) <- 1; let m = set_deg m in [((coef_of_int 1),m)] @@ -464,7 +464,7 @@ let puisP p n= let d = nvar (snd (List.hd p)) in let rec puisP n = match n with - 0 -> [coef1, Array.create (d+1) 0] + 0 -> [coef1, Array.make (d+1) 0] | 1 -> p |_ -> multP p (puisP (n-1)) in puisP n @@ -503,13 +503,13 @@ let lm p = snd (List.hd (ppol p)) let nallpol = ref 0 -let allpol = ref (Array.create 1000 polynom0) +let allpol = ref (Array.make 1000 polynom0) let new_allpol p s = nallpol := !nallpol + 1; if !nallpol >= Array.length !allpol then - allpol := Array.append !allpol (Array.create !nallpol polynom0); + allpol := Array.append !allpol (Array.make !nallpol polynom0); let p = {pol = ref p; num = !nallpol; sugar = s} in !allpol.(!nallpol)<- p; p @@ -1028,7 +1028,7 @@ let in_ideal d lp p = Hashtbl.clear hmon; Hashtbl.clear coefpoldep; nallpol := 0; - allpol := Array.create 1000 polynom0; + allpol := Array.make 1000 polynom0; homogeneous := List.for_all is_homogeneous (p::lp); if !homogeneous then info "homogeneous polynomials\n"; info ("p: "^(stringPcut p)^"\n"); diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml index 638242462..8e2fc07c0 100644 --- a/plugins/nsatz/utile.ml +++ b/plugins/nsatz/utile.ml @@ -81,7 +81,7 @@ let facteurs_liste div constant lp = c est un élément quelconque de E. *) let factorise_tableau div zero c f l1 = - let res = Array.create (Array.length f) (c,[]) in + let res = Array.make (Array.length f) (c,[]) in Array.iteri (fun i p -> let r = ref p in let li = ref [] in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index f98aba0a8..0dd137b6f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1254,7 +1254,7 @@ let replay_history tactic_normalisation = and id2 = hyp_of_tag e2.id in let eq1 = val_of(decompile e1) and eq2 = val_of(decompile e2) in - if k1 =? one & e2.kind = EQUA then + if k1 =? one && e2.kind = EQUA then let tac_thm = match e1.kind with | EQUA -> Lazy.force coq_OMEGA5 diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 800254671..60887b451 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -36,9 +36,9 @@ module MakeOmegaSolver (Int:INT) = struct type bigint = Int.bigint let (?) x y = Int.less_than y x -let (>=?) x y = Int.less_than y x or x = y +let (>=?) x y = Int.less_than y x || x = y let (=?) = (=) let (+) = Int.add let (-) = Int.sub @@ -239,7 +239,7 @@ let add_event, history, clear_history = (fun () -> !accu), (fun () -> accu := []) -let nf_linear = Sort.list (fun x y -> x.v > y.v) +let nf_linear = List.sort (fun x y -> Pervasives.(-) y.v x.v) let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) @@ -301,16 +301,16 @@ let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = end end else let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in - if eq_flag=EQUA & x mod gcd <> zero then begin + if eq_flag=EQUA && x mod gcd <> zero then begin add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE - end else if eq_flag=DISE & x mod gcd <> zero then begin + end else if eq_flag=DISE && x mod gcd <> zero then begin add_event (FORGET_C eq.id); [] end else if gcd <> one then begin let c = floor_div x gcd in let d = x - c * gcd in let new_eq = {id=id; kind=eq_flag; constant=c; body=map_eq_linear (fun c -> c / gcd) e} in - add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd) + add_event (if eq_flag=EQUA || eq_flag = DISE then EXACT_DIVIDE(eq,gcd) else DIVIDE_AND_APPROX(eq,new_eq,gcd,d)); [new_eq] end else [eq] @@ -472,7 +472,7 @@ let select_variable system = Hashtbl.iter (fun v ({contents = c}) -> incr var_cpt; - if c v_lhs := Some (compute_lhs @@ -260,7 +260,7 @@ let compute_ivs gl f cs = end) lci; - if !c_lhs = None & !v_lhs = None then i_can't_do_that (); + if !c_lhs = None && !v_lhs = None then i_can't_do_that (); (* The Cases predicate is a lambda; we assume no dependency *) let p = match kind_of_term p with @@ -295,7 +295,7 @@ binary search trees (see file \texttt{Quote.v}) *) and variables (open terms) *) let rec closed_under cset t = - (ConstrSet.mem t cset) or + (ConstrSet.mem t cset) || (match (kind_of_term t) with | Cast(c,_,_) -> closed_under cset c | App(f,l) -> closed_under cset f && Array.for_all (closed_under cset) l @@ -357,7 +357,7 @@ let path_of_int n = (* This function does not descend under binders (lambda and Cases) *) let rec subterm gl (t : constr) (t' : constr) = - (pf_conv_x gl t t') or + (pf_conv_x gl t t') || (match (kind_of_term t) with | App (f,args) -> Array.exists (fun t -> subterm gl t t') args | Cast(t,_,_) -> (subterm gl t t') diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 75fe49bcf..af833dacb 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -352,7 +352,7 @@ let parse_rel gl t = let is_scalar t = let rec aux t = match destructurate t with - | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> aux t1 & aux t2 + | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> aux t1 && aux t2 | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true | _ -> false in diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index b6fdf315c..180d15009 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -45,7 +45,7 @@ let interp_ascii_string dloc s = let p = if String.length s = 1 then int_of_char s.[0] else - if String.length s = 3 & is_digit s.[0] & is_digit s.[1] & is_digit s.[2] + if String.length s = 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] then int_of_string s else user_err_loc (dloc,"interp_ascii_string", diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index bddca9e65..efbd140ee 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -72,19 +72,19 @@ let bignat_of_r = let rec bignat_of_pos = function (* 1+1 *) | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)]) - when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two + when p = glob_Rplus && o1 = glob_R1 && o2 = glob_R1 -> two (* 1+(1+1) *) | GApp (_,GRef (_,p1), [GRef (_,o1); GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])]) - when p1 = glob_Rplus & p2 = glob_Rplus & - o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three + when p1 = glob_Rplus && p2 = glob_Rplus && + o1 = glob_R1 && o2 = glob_R1 && o3 = glob_R1 -> three (* (1+1)*b *) | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult -> if bignat_of_pos a <> two then raise Non_closed_number; mult_2 (bignat_of_pos b) (* 1+(1+1)*b *) | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])]) - when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1 -> + when p1 = glob_Rplus && p2 = glob_Rmult && o = glob_R1 -> if bignat_of_pos a <> two then raise Non_closed_number; add_1 (mult_2 (bignat_of_pos b)) | _ -> raise Non_closed_number -- cgit v1.2.3