First draft of Parser.problem_of_string

[fireball-separation.git] / ocaml / parser.mli

diff --git a/ocaml/parser.mli b/ocaml/parser.mli
index c205cb293640fc6ef7c40e287971547cc722a113..927506732d13e8c125769d28a4c3dcaf5696c6af 100644 (file)
--- a/ocaml/parser.mli
+++ b/ocaml/parser.mli
@@ -1,10 +1,10 @@
 exception ParsingError of string\r
 \r
-(* parses a string to a term *)\r
-(* val parse: string -> Num.nf *)\r
-(* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *)\r
-val parse_many: string list -> Num.nf list * string list\r
 val parse': string list -> Num.nf list * string list\r
-val parse_problem:\r
+val problem_of_string:\r
  string ->\r
-  Num.i_var option * Num.i_n_var list * Num.i_n_var list\r
+  string (* problem label *)\r
+  * Num.i_var option (* div *)\r
+  * Num.i_n_var list (* conv *)\r
+  * Num.i_n_var list (* ps *)\r
+  * string list (* names of free variables *)\r