From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 15 Jul 2017 13:05:34 +0000 (+0200)
Subject: Fixed "$" in parser
X-Git-Tag: weak-reduction-separation~30
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f7ba4d1225ca4fb09750f3d23b197b8372f1350b;p=fireball-separation.git

Fixed "$" in parser

(cherry picked from commit db562ac015ffc6c1a08c226b4eef7790b21661cd)
---

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 15e2a6a..e410d75 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -237,6 +237,6 @@ let from_file path =
  with End_of_file ->
   close_in chan in
  let txt = String.concat "\n" (List.rev !lines) in
- let problems = Str.split (Str.regexp "\\$") txt in
+ let problems = Str.split (Str.regexp "\n\\$") txt in
  List.map problem_of_string (List.tl (List.map ((^) "$") problems))
 ;;
diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index aed29d6..cd57451 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -17,9 +17,9 @@ let assert_unseparable x =
 
 let assert_depends x =
  let c = String.sub (Lambda4.label_of_problem x) 0 1 in
- prerr_endline(Lambda4.label_of_problem x); assert (c = "!" || c="?");
- let q = c = "!" in
- (if q then assert_separable else assert_unseparable) x
+ if c = "!" then assert_separable x
+  else if c = "?" then assert_unseparable x
+   else (solve x; ())
 ;;
 
 let main () =