--- alt-ergo-2.3.0-free/extra/ocpChecker.ml.orig	2021-06-29 06:08:30.000000000 -0600
+++ alt-ergo-2.3.0-free/extra/ocpChecker.ml	2022-02-23 12:58:05.976390283 -0700
@@ -45,10 +45,10 @@ let update_file file lines =
       exit 2
   in
   Queue.iter (fun line ->
-      Pervasives.output_string cout line;
-      Pervasives.output_string cout "\n"
+      Stdlib.output_string cout line;
+      Stdlib.output_string cout "\n"
     )lines;
-  Pervasives.flush cout;
+  Stdlib.flush cout;
   close_out cout
 
 
--- alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml.orig	2022-05-20 01:34:55.000000000 -0600
+++ alt-ergo-2.3.0-free/sources/tools/gui/annoted_ast.ml	2022-06-18 16:08:13.053310654 -0600
@@ -191,7 +191,7 @@ type annoted_node =
 module MDep = Map.Make (
   struct
     type t = atyped_decl annoted
-    let compare = Pervasives.compare
+    let compare = Stdlib.compare
   end)
 
 
@@ -880,9 +880,9 @@ let find_dep_by_string dep s =
        | None -> begin
            match d.c with
            | ALogic (_, ls, _, _) when List.mem s ls -> Some d
-           | ATypeDecl (_, _, s', _, _) when Pervasives.(=) s s'-> Some d
-           | APredicate_def (_, p, _, _) when Pervasives.(=) s p -> Some d
-           | AFunction_def (_, f, _, _, _, _) when Pervasives.(=) s f -> Some d
+           | ATypeDecl (_, _, s', _, _) when Stdlib.(=) s s'-> Some d
+           | APredicate_def (_, p, _, _) when Stdlib.(=) s p -> Some d
+           | AFunction_def (_, f, _, _, _, _) when Stdlib.(=) s f -> Some d
            | _ -> None
          end
     ) dep None
@@ -892,7 +892,7 @@ let find_tag_deps dep tag =
     (fun d (deps,_) found ->
        match found with
        | Some _ -> found
-       | None -> if Pervasives.(=) d.tag tag then Some deps else None
+       | None -> if Stdlib.(=) d.tag tag then Some deps else None
     ) dep None
 
 let find_tag_inversedeps dep tag =
@@ -900,7 +900,7 @@ let find_tag_inversedeps dep tag =
     (fun d (_,deps) found ->
        match found with
        | Some _ -> found
-       | None -> if Pervasives.(=) d.tag tag then Some deps else None
+       | None -> if Stdlib.(=) d.tag tag then Some deps else None
     ) dep None
 
 let make_dep_string d ex dep s =
@@ -2046,7 +2046,7 @@ and findtags_aform sl aform acc =
         (fun sl (sy, _) ->
            let s = Symbols.to_string_clean sy in
            List.fold_left
-             (fun l s' -> if Pervasives.(=) s' s then l else s'::l) [] sl
+             (fun l s' -> if Stdlib.(=) s' s then l else s'::l) [] sl
         )sl l
     in
     findtags_aform sl aaf.c acc
--- alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml.orig	2022-05-20 01:34:55.000000000 -0600
+++ alt-ergo-2.3.0-free/sources/tools/gui/connected_ast.ml	2022-06-18 16:08:37.469375133 -0600
@@ -388,7 +388,7 @@ let rec unquantify_aform (buffer:sbuffer
         List.fold_left (fun (nbv, used, goal_used, ve, uplet, lets) v ->
             let ((s, _) as v'), e = List.hd ve in
             let cdr_ve = List.tl ve in
-            assert (Pervasives.(=) v v');
+            assert (Stdlib.(=) v v');
             if String.length e == 0 then
               (v'::nbv, used, goal_used, cdr_ve, v'::uplet, lets)
             else
@@ -545,7 +545,7 @@ let rec add_instance_aux ?(register=true
     make_instance env.inst_buffer vars entries af goal_form tyenv in
   let ln_form = least_nested_form used_vars goal_form in
   env.inst_buffer#place_cursor  ~where:env.inst_buffer#end_iter;
-  if Pervasives.(=) ln_form (Exists goal_form) then begin
+  if Stdlib.(=) ln_form (Exists goal_form) then begin
     let hy =
       AAxiom (loc, (sprintf "%s%s" "_instance_" aname), ax_kd, instance.c) in
     let ahy = new_annot env.inst_buffer hy instance.id ptag in
@@ -739,7 +739,7 @@ and add_trigger ?(register=true) t qid e
         if register then
           save env.actions
             (AddTrigger (qf.id,
-                         Pervasives.(=) sbuf env.inst_buffer, str));
+                         Stdlib.(=) sbuf env.inst_buffer, str));
         commit_tags_buffer sbuf
       | _ -> assert false
     end
--- alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml.orig	2022-05-20 01:34:55.000000000 -0600
+++ alt-ergo-2.3.0-free/sources/tools/gui/main_gui.ml	2022-06-18 16:09:14.324472461 -0600
@@ -151,7 +151,7 @@ let save_session envs =
 
 let save_dialog cancel envs () =
   if List.exists
-      (fun env -> Pervasives.(<>) env.actions env.saved_actions) envs then
+      (fun env -> Stdlib.(<>) env.actions env.saved_actions) envs then
     if List.exists
         (fun env -> not (Gui_session.safe_session env.actions)) envs then
       GToolbox.message_box
@@ -250,7 +250,7 @@ let pop_model sat_env () =
 let compare_rows icol_number (model:#GTree.model) row1 row2 =
   let t1 = model#get ~row:row1 ~column:icol_number in
   let t2 = model#get ~row:row2 ~column:icol_number in
-  Pervasives.compare t1 t2
+  Stdlib.compare t1 t2
 
 
 let empty_inst_model () =
@@ -382,7 +382,7 @@ let refresh_timers t () =
   let total =
     tsat +. tmatch +. tcc +. tarith +. tarrays +. tsum +. trecords +. tac in
 
-  let total = if Pervasives.(=) total 0. then 1. else total in
+  let total = if Stdlib.(=) total 0. then 1. else total in
 
   t.tl_sat#set_text (sprintf "%3.2f s" tsat);
   t.tl_match#set_text (sprintf "%3.2f s" tmatch);
@@ -455,7 +455,7 @@ let add_inst ({ h; _ } as inst_model) or
   let id = Expr.id orig in
   let name =
     match Expr.form_view orig with
-    | Expr.Lemma { Expr.name = n ; _ } when Pervasives.(<>) n "" -> n
+    | Expr.Lemma { Expr.name = n ; _ } when Stdlib.(<>) n "" -> n
     | Expr.Lemma _ | Expr.Unit _ | Expr.Clause _ | Expr.Literal _
     | Expr.Skolem _ | Expr.Let _ | Expr.Iff _ | Expr.Xor _ ->
       string_of_int id
@@ -607,7 +607,7 @@ let vt_signal =
 
 let force_interrupt old_action_ref n =
   (* This function is called just before the thread's timeslice ends *)
-  if Pervasives.(=) (Some (Thread.id(Thread.self()))) !interrupt then
+  if Stdlib.(=) (Some (Thread.id(Thread.self()))) !interrupt then
     raise Abort_thread;
   match !old_action_ref with
   | Sys.Signal_handle f -> f n
@@ -723,8 +723,8 @@ let remove_context env () =
          toggle_prune env td
        | AAxiom (_, s, _, _)
          when String.length s = 0 ||
-              (Pervasives.(<>) s.[0] '_'  &&
-               Pervasives.(<>) s.[0] '@') ->
+              (Stdlib.(<>) s.[0] '_'  &&
+               Stdlib.(<>) s.[0] '@') ->
          toggle_prune env td
        | _ -> ()
     ) env.ast
@@ -951,7 +951,7 @@ let search_all entry (_sv:GSourceView2.s
   buf#remove_tag found_all_tag ~start:buf#start_iter ~stop:buf#end_iter;
   let str = entry#text in
   let iter = ref buf#start_iter in
-  if Pervasives.(<>) str "" then
+  if Stdlib.(<>) str "" then
     let result = ref None in
     search_one buf str result iter found_all_tag;
     while !result != None do
@@ -1300,7 +1300,7 @@ let start_gui all_used_context =
 
   let set_wrap_lines _ =
     List.iter (fun env ->
-        if Pervasives.(=) env.goal_view#wrap_mode `NONE then (
+        if Stdlib.(=) env.goal_view#wrap_mode `NONE then (
           env.goal_view#set_wrap_mode `CHAR;
           env.inst_view#set_wrap_mode `CHAR;
           Gui_config.update_wrap true