From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 31 May 2018 21:45:14 +0000 (+0200)
Subject: Make the code OCaml-4.06.1-friendly
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5664c5924f59c805c6e658698cc2fa535cab27f6;p=fireball-separation.git

Make the code OCaml-4.06.1-friendly
---

diff --git a/ocaml/Makefile b/ocaml/Makefile
index 3a94a7a..2557224 100644
--- a/ocaml/Makefile
+++ b/ocaml/Makefile
@@ -13,8 +13,8 @@ a.out: $(UTILS) lambda4.cmx
 test4.out: $(UTILS) lambda4.cmx test.ml
 	$(OCAMLC) -o test4.out $(LIB) $^
 
-simple.out: $(UTILS) simple.ml
-	$(OCAMLC) -o simple.out $(LIB) $(UTILS) simple.ml
+simple.out: $(UTILS) simple.cmx
+	$(OCAMLC) -o simple.out $(LIB) $^
 
 simple_test.out: $(UTILS) simple.cmx simple_test.ml
 	$(OCAMLC) -o simple_test.out $(LIB) $^
diff --git a/ocaml/console.ml b/ocaml/console.ml
index 696a74d..f3fbef6 100644
--- a/ocaml/console.ml
+++ b/ocaml/console.ml
@@ -40,7 +40,7 @@ let cols =
 ;;
 
 let writeall s =
-  let _ = Unix.send socket s 0 (String.length s) [] in ()
+  let _ = Unix.send socket (Bytes.of_string s) 0 (String.length s) [] in ()
 ;;
 
 let concat ls = (String.concat sepx ls) ^ endx;;
diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 90a91e0..83c1b1d 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -39,7 +39,7 @@ let label_of_problem {label} = label;;
 let string_of_var l x =
  try
   List.nth l x
- with Failure "nth" -> "`" ^ string_of_int x
+ with Failure _ -> "`" ^ string_of_int x
 ;;
 let string_of_term p t = print ~l:p.var_names (t :> nf);;
 
diff --git a/ocaml/num.ml b/ocaml/num.ml
index 8ecf124..cc30cb5 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -123,7 +123,7 @@ end
 
 (* let rec string_of_term l  = fun _ -> "";; *)
 
-let rec string_of_term =
+let string_of_term =
  let boundvar x = "v" ^ string_of_int x in
  let varname lev l n =
   if n < lev then boundvar (lev-n-1)
@@ -148,7 +148,8 @@ let rec string_of_term =
  and string_of_term_no_pars lev l = function
   | `Lam _ as t -> string_of_term_no_pars_lam lev l t
   | #nf as t -> string_of_term_no_pars_app lev l t
- in string_of_term_no_pars 0
+ and string_of_term t = string_of_term_no_pars 0 t in
+ string_of_term
 ;;
 
 let print ?(l=[]) = string_of_term l;;
diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 1dd4b58..8003226 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -30,11 +30,11 @@ let explode s =
 ;;
 
 let implode l =
-  let res = String.create (List.length l) in
+  let res = Bytes.create (List.length l) in
   let rec aux i = function
     | [] -> res
-    | c :: l -> res.[i] <- c; aux (i + 1) l in
-  aux 0 l
+    | c :: l -> Bytes.set res i c; aux (i + 1) l in
+  Bytes.to_string (aux 0 l)
 ;;
 
 let rec strip_spaces = function
diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 3bd7ec4..e04b4ea 100644
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -115,7 +115,7 @@ in
         (try
           let e,t,s' = List.nth e n in
           aux g (e,t,s'@s)
-         with Invalid_argument "List.nth" | Failure _ -> m
+         with Invalid_argument _ | Failure _ -> m
          )
      | (e, B, _) -> (e, B, [])
      | (e, L t, []) ->
diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 991779e..8e4f619 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -288,9 +288,6 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")")
  sanity p
 ;;
 
-;;
-
-
 let rec auto p =
  let hd_var, n_args = get_inert p.div in
  match get_subterm_with_head_and_args hd_var n_args p.conv with