X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fparser.mli;h=927506732d13e8c125769d28a4c3dcaf5696c6af;hb=1b3b3eb5c68d4b1ca28ef911b81e6757db080187;hp=c073c3af1a7436e537381ea6b88b234a5735dc49;hpb=e4aa4a66dd0a4946607245a0f43eab803f2770c4;p=fireball-separation.git

diff --git a/ocaml/parser.mli b/ocaml/parser.mli
index c073c3a..9275067 100644
--- a/ocaml/parser.mli
+++ b/ocaml/parser.mli
@@ -1,9 +1,10 @@
-type term =
-  | Var of int
-  | App of term * term
-  | Lam of term
+exception ParsingError of string
 
-(* parses a string to a term *)
-val parse: string -> term
-(* 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 -> term list * string list
+val parse': string list -> Num.nf list * string list
+val problem_of_string:
+ 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 *)