-val qualify: MatitaTypes.status -> string -> string
-
-val get_current_proof: MatitaTypes.status -> ProofEngineTypes.proof
-val get_stack: MatitaTypes.status -> Continuationals.Stack.t
-val set_stack: Continuationals.Stack.t ->MatitaTypes.status ->MatitaTypes.status
-val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv
-
-val get_proof_context:
- MatitaTypes.status -> ProofEngineTypes.goal -> Cic.context
-
-val get_proof_conclusion:
- MatitaTypes.status -> ProofEngineTypes.goal -> Cic.term
-