X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fparser.mli;h=d131edbf79b65b46315d19510ec9e96583b9f58e;hb=4674dd787b5141c8aa22339d497ba671f4435da5;hp=c205cb293640fc6ef7c40e287971547cc722a113;hpb=2c278a1d49aa0db5211821c1c9eec27212e5e53c;p=fireball-separation.git

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