+type command_outcome = bool * bool
+
+type script_item =
+ [ `Tactic
+ | `Theorem
+ | `Qed of UriManager.uri
+ | `Def of UriManager.uri
+ | `Inductive of UriManager.uri
+ ]
+
+class type interpreter =
+ object
+ method evalAst : DisambiguateTypes.tactical -> command_outcome
+ method evalPhrase : string -> command_outcome
+(* method evalStream: char Stream.t -> command_outcome *)
+ method endOffset : int
+ method lastItem: script_item option
+ method setState: [`Proof | `Command] -> unit
+ method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
+ end
+
+type term_source =
+ [ `Ast of DisambiguateTypes.term
+ | `Cic of Cic.term * Cic.metasenv
+ | `String of string
+ ]
+
+class type mathViewer =
+ object
+ method checkTerm: term_source -> unit
+ end
+
+class type cicBrowser =
+ object
+ method loadUri: string -> unit
+ method loadTerm: term_source -> unit
+ end
+
+type mml_of_cic_sequent =
+ Cic.metasenv -> Cic.conjecture ->
+ Gdome.document *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (string, Cic.hypothesis) Hashtbl.t)
+
+type mml_of_cic_object =
+ explode_all:bool -> UriManager.uri -> Cic.annobj ->
+ (string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t ->
+ Gdome.document
+
+type namer = ProofEngineTypes.mk_fresh_name_type
+
+let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ =
+ raise (Failure "ambiguous input")
+let mono_interp_callback _ = raise (Failure "ambiguous input")