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"
?context:Cic.context -> ?metasenv:Cic.metasenv ->
?env:DisambiguateTypes.environment ->
char Stream.t ->
- (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph)
(** @param env @see disambiguateTerm above *)
method disambiguateTermAst:
?context:Cic.context -> ?metasenv:Cic.metasenv ->
?env:DisambiguateTypes.environment ->
DisambiguateTypes.term ->
- (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph)
end
(*
(** parse a single phrase contained in the input string. Additional
* garbage at the end of the phrase is ignored
- * @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 true if no exception has been raised by the evaluation, false
+ * otherwise
*)
- method evalPhrase: ?transparent:bool -> string -> unit
+ method evalPhrase: string -> bool
+
+ (** as above, evaluating a command/tactics AST *)
+ method evalAst: 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} *)