+exception Cancel
+exception Unbound_identifier of string
+
+(*
+let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
+let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
+
+let unopt_uri ?(kind = `Con) = function
+ | Some uri -> uri
+ | None ->
+ (match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri)
+*)
+let unopt_uri = function Some uri -> uri | None -> assert false
+
+class type parserr = (* "parser" is a keyword :-( *)
+ object
+ method parseTerm: char Stream.t -> DisambiguateTypes.term
+ method parseTactical: char Stream.t -> DisambiguateTypes.tactical
+ end
+
+class type console =
+ object
+ method echo_message : string -> unit
+ method echo_error : string -> unit
+ method clear : unit -> unit
+ method wrap_exn : 'a. (unit -> 'a) -> 'a option
+ method choose_uri : string list -> string
+ method show : ?msg:string -> unit -> unit
+ end
+
+type choose_uris_callback =
+ selection_mode:[`MULTIPLE|`SINGLE] ->
+ ?title:string -> ?msg:string -> ?nonvars_button:bool ->
+ string list ->
+ string list
+type choose_interp_callback = (string * string) list list -> int list
+
+class type disambiguator =
+ object
+ method env: DisambiguateTypes.environment
+ method setEnv: DisambiguateTypes.environment -> unit
+
+ method chooseUris: choose_uris_callback
+ method setChooseUris: choose_uris_callback -> unit
+
+ method chooseInterp: choose_interp_callback
+ method setChooseInterp: choose_interp_callback -> unit
+
+ method parserr: parserr
+
+ method disambiguateTerm:
+ ?context:Cic.context -> ?metasenv:Cic.metasenv ->
+ ?env:DisambiguateTypes.environment ->
+ char Stream.t ->
+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term *
+ CicUniv.universe_graph)
+ method disambiguateTermAst:
+ ?context:Cic.context -> ?metasenv:Cic.metasenv ->
+ ?env:DisambiguateTypes.environment ->
+ DisambiguateTypes.term ->
+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term *
+ CicUniv.universe_graph)
+
+ method disambiguateTermAsts:
+ ?metasenv:Cic.metasenv ->
+ ?env:DisambiguateTypes.environment ->
+ DisambiguateTypes.term list ->
+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
+ CicUniv.universe_graph)
+ end
+
+class type proof =