snapshot:

[helm.git] / helm / matita / matitaTypes.ml

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 20ffd350dfd3d1965c8b62e524797d7065367308..9ae5cc7a98f568c978129682e1380a25e8b8b992 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -36,6 +36,7 @@ let debug_print s =
 exception No_proof  (** no current proof is available *)
 
 exception Cancel
+exception Unbound_identifier of string
 
 (*
 let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
@@ -132,20 +133,17 @@ class type interpreter =
       * @param transparent per default the interpreter catch all exceptions ans
       * prints them in the console. When transparent is set to true exceptions
       * are flow through. Defaults to false
+      * @return success value of the interpretation
       *)
-    method evalPhrase: ?transparent:bool -> string -> unit
+    method evalPhrase: ?transparent:bool -> string -> bool
+
+    method evalAst: ?transparent:bool -> DisambiguateTypes.tactical -> bool
 
       (** offset from the starting of the last string parser by evalPhrase where
       * parsing stop.
       * @raise Failure when no offset has been recorded *)
     method endOffset: int
 
-(*
-      (** undo last steps phrases.
-      * @param steps number of phrases to undo; defaults to 1 *)
-    method undo: ?steps:int -> unit -> unit
-*)
-
   end
 
 (** {2 MathML widgets} *)