propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / bin / recomm / mrcInput.ml

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml
index c5d7f585772a9caf4b54597f56e003c162873bcb..e31efac1f9a3134168f6c9fe34c279c812b38844 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml
@@ -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 =