X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems.ml;h=f2812775b2a3dc43dcf94e210ead6076e6b1c011;hb=666a228779e465d08a0deea2e35c0cccf5722b40;hp=0374b4787472f9ac910f778c90bea30d28b43f62;hpb=dfad242808c3525a0d9e3420565551964fcf0832;p=fireball-separation.git

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 0374b47..f281277 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -1,6 +1,22 @@
 open Lambda4;;
 open Util;;
 
+(* Syntax for problem files in problem/ folder:
+
+- dollar ($) on newline
+  begin new problem
+  $! means that the problem is expected to be separable,
+  $? means that it is expected to be unseparable
+
+- (#) on new line
+  comment line
+
+- (D) (C) (N) stand respectively for divergent, convergent, numeric
+
+- lines starting with spaces inherit the type from the last line
+
+*)
+
 let assert_separable x =
  match solve x with
  | _, `Separable _ -> ()
@@ -17,9 +33,9 @@ let assert_unseparable x =
 
 let assert_depends x =
  let c = String.sub (Lambda4.label_of_problem (fst x)) 0 1 in
- prerr_endline(Lambda4.label_of_problem (fst 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 () =