From baaf1f92ccd473294679dd9025c3ae9a441a82fa Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 16 Oct 2023 15:58:09 +0200
Subject: [PATCH] Minor patch for 4.08 compat

---
 src/standard/misc.ml      | 8 ++++++++
 src/standard/misc.mli     | 2 ++
 src/standard/statement.ml | 2 +-
 3 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/standard/misc.ml b/src/standard/misc.ml
index 77f3a2233..3668b17d7 100644
--- a/src/standard/misc.ml
+++ b/src/standard/misc.ml
@@ -170,6 +170,14 @@ let rec print_list ~print_sep ~sep ~print fmt = function
       print h print_sep sep
       (print_list ~print_sep ~sep ~print) r
 
+let list_concat_map f l =
+  let rec aux f acc = function
+    | [] -> List.rev acc
+    | x :: l ->
+       let xs = f x in
+       aux f (List.rev_append xs acc) l
+  in aux f [] l
+
 
 (* Iteration *)
 (* ************************************************************************* *)
diff --git a/src/standard/misc.mli b/src/standard/misc.mli
index 94cb18cb7..6e89931f0 100644
--- a/src/standard/misc.mli
+++ b/src/standard/misc.mli
@@ -68,6 +68,8 @@ val print_list :
 val foldn : int -> ('a -> 'a) -> 'a -> 'a
 (** Applies the given function [n] times. *)
 
+val list_concat_map : ('a -> 'b list) -> 'a list -> 'b list
+(** Same as {List.concat_map} (which is not available on ocaml.4.08). *)
 
 (** {2 Lexbuf helpers} *)
 
diff --git a/src/standard/statement.ml b/src/standard/statement.ml
index 646f50c84..53d84878d 100644
--- a/src/standard/statement.ml
+++ b/src/standard/statement.ml
@@ -643,7 +643,7 @@ let cnf ?loc ?annot id role t =
     match t with
     | { Term.term = Term.App
             ({ Term.term = Term.Builtin Term.Or; _ }, l); _ } ->
-      List.concat_map split_or l
+      Misc.list_concat_map split_or l
     | _ -> [t]
   in
   tptp ?loc ?annot "cnf" id role (`Clause (split_or t))