]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml
Porting to ocaml 5
[helm.git] / matita / matita / contribs / lambdadelta / bin / recomm / mrcInput.ml
index c5d7f585772a9caf4b54597f56e003c162873bcb..2d6e3b431046ca6be164f7411e3fb1b5326eb5e4 100644 (file)
@@ -1,14 +1,11 @@
 module ET = MrcTypes
+module RL = RecommLib
 
 let read_substs substs ich =
-  let map subst =
-    let words = String.split_on_char ' ' subst in
-    List.filter ((<>) "") words
-  in
   while true do
     let line = input_line ich in
-    let subst = String.split_on_char ',' line in   
-    substs := List.map map subst :: !substs
+    let subst = RL.split_on_char ',' line in
+    substs := List.map (RL.split_on_char ' ') subst :: !substs
   done
 
 let read_file file =
@@ -44,7 +41,7 @@ let read_dir file =
     Filename.remove_extension name
   in
   let dir = Array.to_list (Sys.readdir file) in
-  let mods = List.fast_sort Pervasives.compare (list_rev_filter_map filter map dir) in
+  let mods = List.fast_sort Stdlib.compare (list_rev_filter_map filter map dir) in
   {
     ET.cdir = file; mods;
   }
@@ -65,7 +62,7 @@ let read_index dir =
     try read_mods mods ich with
     | End_of_file -> close_in ich 
   end;
-  let mods = List.fast_sort Pervasives.compare !mods in
+  let mods = List.fast_sort Stdlib.compare !mods in
   {
     ET.cdir = dir; mods;
   }