aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/common.ml2
-rw-r--r--plugins/ltac/profile_ltac.ml2
-rw-r--r--plugins/ltac/tactic_debug.ml2
-rw-r--r--plugins/micromega/certificate.ml2
-rw-r--r--plugins/micromega/coq_micromega.ml4
-rw-r--r--plugins/micromega/csdpcert.ml2
-rw-r--r--plugins/micromega/mfourier.ml4
-rw-r--r--plugins/micromega/mutils.ml4
-rw-r--r--plugins/micromega/polynomial.ml16
-rw-r--r--plugins/micromega/simplex.ml4
-rw-r--r--plugins/micromega/sos_lib.ml10
-rw-r--r--plugins/micromega/vect.ml4
-rw-r--r--plugins/omega/coq_omega.ml6
-rw-r--r--plugins/omega/omega.ml2
-rw-r--r--plugins/ssr/ssrview.ml2
15 files changed, 33 insertions, 33 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9abf212443..109125702c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -125,7 +125,7 @@ module KOrd =
struct
type t = kind * string
let compare (k1, s1) (k2, s2) =
- let c = Pervasives.compare k1 k2 (* OK *) in
+ let c = pervasives_compare k1 k2 (* OK *) in
if c = 0 then String.compare s1 s2
else c
end
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 243e0e945c..9d46bbc74e 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -376,7 +376,7 @@ let get_local_profiling_results () = List.hd Local.(!stack)
own. *)
module DData = struct
type t = Feedback.doc_id * Stateid.t
- let compare x y = Pervasives.compare x y
+ let compare x y = compare x y
end
module SM = Map.Make(DData)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 9e735e0680..539536911c 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -156,7 +156,7 @@ let rec prompt level =
begin
let open Proofview.NonLogical in
Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
- if Pervasives.(!batch) then return (DebugOn (level+1)) else
+ if Util.(!batch) then return (DebugOn (level+1)) else
let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
Proofview.NonLogical.catch Proofview.NonLogical.read_line
begin function (e, info) -> match e with
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 2e32b00c25..24039c93c6 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -93,7 +93,7 @@ let dev_form n_spec p =
let rec fixpoint f x =
let y' = f x in
- if Pervasives.(=) y' x then y'
+ if (=) y' x then y'
else fixpoint f y'
let rec_simpl_cone n_spec e =
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index f0435126aa..5cc2c2e061 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1585,7 +1585,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
let hyps_idx = prover.hyps prf in
let hyps = selecti hyps_idx old_cl in
- is_sublist Pervasives.(=) hyps new_cl in
+ is_sublist (=) hyps new_cl in
@@ -1953,7 +1953,7 @@ open Persistent_cache
module Cache = PHashtable(struct
type t = (provername * micromega_polys)
- let equal = Pervasives.(=)
+ let equal = (=)
let hash = Hashtbl.hash
end)
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index d8f71cda0c..cf5f60fb55 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -136,7 +136,7 @@ let pure_sos l =
I should nonetheless be able to try something - over Z > is equivalent to -1 >= *)
try
let l = List.combine l (CList.interval 0 (List.length l -1)) in
- let (lt,i) = try (List.find (fun (x,_) -> Pervasives.(=) (snd x) Mc.Strict) l)
+ 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
let (n,polys) = sumofsquares plt in (* n * (ci * pi^2) *)
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 34fb32c270..943bcb384b 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -15,7 +15,7 @@ open Vect
let debug = false
-let compare_float (p : float) q = Pervasives.compare p q
+let compare_float (p : float) q = pervasives_compare p q
(** Implementation of intervals *)
open Itv
@@ -587,7 +587,7 @@ struct
let optimise vect l =
(* We add a dummy (fresh) variable for vector *)
let fresh =
- List.fold_left (fun fr c -> Pervasives.max fr (Vect.fresh c.coeffs)) 0 l in
+ List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in
let cstr = {
coeffs = Vect.set fresh (Int (-1)) vect ;
op = Eq ;
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 97cf23ac1f..537b6175b4 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -21,7 +21,7 @@
module Int = struct
type t = int
- let compare : int -> int -> int = Pervasives.compare
+ let compare : int -> int -> int = compare
let equal : int -> int -> bool = (=)
end
@@ -354,7 +354,7 @@ struct
let from i = i
let next i = i + 1
- let max : int -> int -> int = Pervasives.max
+ let max : int -> int -> int = max
let pp o i = output_string o (string_of_int i)
let compare : int -> int -> int = Int.compare
let to_int x = x
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index f909b4ecda..1a31a36732 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -278,7 +278,7 @@ and op = |Eq | Ge | Gt
exception Strict
-let is_strict c = Pervasives.(=) c.op Gt
+let is_strict c = (=) c.op Gt
let eval_op = function
| Eq -> (=/)
@@ -422,7 +422,7 @@ module LinPoly = struct
let min_list (l:int list) =
match l with
| [] -> None
- | e::l -> Some (List.fold_left Pervasives.min e l)
+ | e::l -> Some (List.fold_left min e l)
let search_linear p l =
min_list (search_all_linear p l)
@@ -656,9 +656,9 @@ module ProofFormat = struct
let rec compare p1 p2 =
match p1, p2 with
| Annot(s1,p1) , Annot(s2,p2) -> if s1 = s2 then compare p1 p2
- else Pervasives.compare s1 s2
- | Hyp i , Hyp j -> Pervasives.compare i j
- | Def i , Def j -> Pervasives.compare i j
+ else Util.pervasives_compare s1 s2
+ | Hyp i , Hyp j -> Util.pervasives_compare i j
+ | Def i , Def j -> Util.pervasives_compare i j
| Cst n , Cst m -> Num.compare_num n m
| Zero , Zero -> 0
| Square v1 , Square v2 -> Vect.compare v1 v2
@@ -667,7 +667,7 @@ module ProofFormat = struct
| MulPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2)
| AddPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2)
| CutPrf p , CutPrf p' -> compare p p'
- | _ , _ -> Pervasives.compare (id_of_constr p1) (id_of_constr p2)
+ | _ , _ -> Util.pervasives_compare (id_of_constr p1) (id_of_constr p2)
end
@@ -785,7 +785,7 @@ module ProofFormat = struct
let rec xid_of_hyp i l' =
match l' with
| [] -> failwith (Printf.sprintf "id_of_hyp %i %s" hyp (string_of_int_list l))
- | hyp'::l' -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l' in
+ | hyp'::l' -> if (=) hyp hyp' then i else xid_of_hyp (i+1) l' in
xid_of_hyp 0 l
end
@@ -873,7 +873,7 @@ module ProofFormat = struct
let (p,o) = eval_prf_rule (fun i -> IMap.find i env) prf in
if is_unsat (p,o) then true
else
- if Pervasives.(=) rst Done
+ if (=) rst Done
then
begin
Printf.fprintf stdout "Last inference %a %s\n" LinPoly.pp p (string_of_op o);
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index 15fb55c007..4c95e6da75 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -587,7 +587,7 @@ let cut env rmin sol vm (rst:Restricted.t) tbl (x,v) =
Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x;
Printf.printf " %a\n" WithProof.output (v,prf);
end;
- if Pervasives.(=) (snd v) Eq
+ if (=) (snd v) Eq
then (* Unsat *) Some (x,(v,prf))
else
let vl = (Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol)) in
@@ -651,7 +651,7 @@ let integer_solver lp =
match find_cut (!nb mod 2) env cr (*x*) sol vm rst tbl with
| None -> None
| Some(cr,((v,op),cut)) ->
- if Pervasives.(=) op Eq
+ if (=) op Eq
then (* This is a contradiction *)
Some(Step(vr,CutPrf cut, Done))
else
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index e3a9f6f60f..58d5d7ecf1 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -13,7 +13,7 @@ open Num
(* Comparisons that are reflexive on NaN and also short-circuiting. *)
(* ------------------------------------------------------------------------- *)
-let cmp = Pervasives.compare (** FIXME *)
+let cmp = compare (** FIXME *)
let (=?) = fun x y -> cmp x y = 0;;
let (<?) = fun x y -> cmp x y < 0;;
@@ -491,21 +491,21 @@ let temp_path = Filename.get_temp_dir_name ();;
(* ------------------------------------------------------------------------- *)
let strings_of_file filename =
- let fd = try Pervasives.open_in filename
+ let fd = try open_in filename
with Sys_error _ ->
failwith("strings_of_file: can't open "^filename) in
let rec suck_lines acc =
- try let l = Pervasives.input_line fd in
+ try let l = input_line fd in
suck_lines (l::acc)
with End_of_file -> List.rev acc in
let data = suck_lines [] in
- (Pervasives.close_in fd; data);;
+ (close_in fd; data);;
let string_of_file filename =
String.concat "\n" (strings_of_file filename);;
let file_of_string filename s =
- let fd = Pervasives.open_out filename in
+ let fd = open_out filename in
output_string fd s; close_out fd;;
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index 4b2bc66eb7..a5f3b83c48 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -148,7 +148,7 @@ let rec add (ve1:t) (ve2:t) =
match ve1 , ve2 with
| [] , v | v , [] -> v
| (v1,c1)::l1 , (v2,c2)::l2 ->
- let cmp = Pervasives.compare v1 v2 in
+ let cmp = Util.pervasives_compare v1 v2 in
if cmp == 0 then
let s = add_num c1 c2 in
if eq_num (Int 0) s
@@ -163,7 +163,7 @@ let rec xmul_add (n1:num) (ve1:t) (n2:num) (ve2:t) =
| [] , _ -> mul n2 ve2
| _ , [] -> mul n1 ve1
| (v1,c1)::l1 , (v2,c2)::l2 ->
- let cmp = Pervasives.compare v1 v2 in
+ let cmp = Util.pervasives_compare v1 v2 in
if cmp == 0 then
let s = ( n1 */ c1) +/ (n2 */ c2) in
if eq_num (Int 0) s
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 6aec83318c..776bd0a829 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -500,7 +500,7 @@ let context sigma operation path (t : constr) =
| (p, Fix ((_,n as ln),(tys,lna,v))) ->
let l = Array.length v in
let v' = Array.copy v in
- v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
+ v'.(n)<- loop (Util.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
| ((P_TYPE :: p), Prod (n,t,c)) ->
(mkProd (n,loop i p t,c))
| ((P_TYPE :: p), Lambda (n,t,c)) ->
@@ -684,7 +684,7 @@ let simpl_coeffs path_init path_k =
| _ -> assert false)
| _ -> assert false
in
- let n = Pervasives.(-) (List.length path_k) (List.length path_init) in
+ let n = Util.(-) (List.length path_k) (List.length path_init) in
let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl)
in
convert_concl ~check:false newc DEFAULTcast
@@ -1000,7 +1000,7 @@ let shrink_pair p f1 f2 =
| t1,t2 ->
begin
oprint t1; print_newline (); oprint t2; print_newline ();
- flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1")
+ flush stdout; CErrors.user_err Pp.(str "shrink.1")
end
let reduce_factor p = function
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index cec87221f0..05c31062fc 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -242,7 +242,7 @@ let add_event, history, clear_history =
(fun () -> !accu),
(fun () -> accu := [])
-let nf_linear = List.sort (fun x y -> Pervasives.(-) y.v x.v)
+let nf_linear = List.sort (fun x y -> Util.(-) y.v x.v)
let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x))
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 34f13b1096..f91b5e7aa2 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -26,7 +26,7 @@ module AdaptorDb = struct
module AdaptorKind = struct
type t = kind
- let compare = Pervasives.compare
+ let compare = pervasives_compare
end
module AdaptorMap = Map.Make(AdaptorKind)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:26:21 +0000