class interpreter:
disambiguator:MatitaTypes.disambiguator ->
+ proof_handler:MatitaTypes.proof_handler ->
console:MatitaConsole.console ->
- get_proof:(unit -> MatitaTypes.proof) ->
- new_proof:(MatitaTypes.proof -> unit) ->
unit ->
MatitaTypes.interpreter