Moved parse' from Num to Parser

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

diff --git a/ocaml/parser.mli b/ocaml/parser.mli
index c073c3af1a7436e537381ea6b88b234a5735dc49..c205cb293640fc6ef7c40e287971547cc722a113 100644 (file)
--- a/ocaml/parser.mli
+++ b/ocaml/parser.mli
@@ -1,9 +1,10 @@
-type term =\r
-  | Var of int\r
-  | App of term * term\r
-  | Lam of term\r
+exception ParsingError of string\r
 \r
 (* parses a string to a term *)\r
-val parse: string -> 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 -> term list * string list\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
+ string ->\r
+  Num.i_var option * Num.i_n_var list * Num.i_n_var list\r