exception Option_error of string * string
exception Unbound_identifier of string
+type incomplete_proof = {
+ proof: ProofEngineTypes.proof;
+ stack: Continuationals.Stack.t;
+}
+
type proof_status =
No_proof
- | Incomplete_proof of ProofEngineTypes.status
+ | Incomplete_proof of incomplete_proof
| Proof of ProofEngineTypes.proof
| Intermediate of Cic.metasenv
method show_uri_list :
?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end
+
+val qualify: status -> string -> string
+
+val get_current_proof: status -> ProofEngineTypes.proof
+val get_proof_metasenv: status -> Cic.metasenv
+val get_proof_context: status -> ProofEngineTypes.goal -> Cic.context
+val get_proof_conclusion: status -> ProofEngineTypes.goal -> Cic.term
+val get_stack: status -> Continuationals.Stack.t
+
+val set_stack: Continuationals.Stack.t -> status -> status
+