new tacticals

[helm.git] / helm / matita / matitaTypes.mli

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 144c0c1f2b6212a38d0bc4df6923f5cfa36e429f..e425519c6434242d593619175c85a34fb89c8156 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -33,9 +33,14 @@ val command_error : string -> 'a
 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