- method wrap_exn : 'a. (unit -> 'a) -> 'a option
- end
-
-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
-
- (* TODO Zack: as long as matita doesn't support MDI inteface,
- * disambiguateTerm will return a single term *)
- (** @param env disambiguation environment. If this parameter is given the
- * disambiguator act statelessly, that is internal disambiguation status
- * want be changed but only returned. If this parameter is not given the
- * internal one will be used and updated with the disambiguation status
- * resulting from the disambiguation *)
- method disambiguateTerm :
- ?context:Cic.context ->
- ?metasenv:Cic.metasenv ->
- ?env:DisambiguateTypes.environment ->
- char Stream.t ->
- 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 *
- CicUniv.universe_graph
-
- (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All
- * AST should be closed hence no context param is permitted on this method
- *)
- 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 =
- object
- inherit [unit] StatefulProofEngine.status
-
- (** return a pair of "xml" (as defined in Xml module) representing the *
- * current proof type and body, respectively *)
- method toXml : Xml.token Stream.t * Xml.token Stream.t
-
- method toString : string