new tacticals

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 8b4cb1f9deeadf80ddaa69034811ec566c76bed0..29fefca03f9563a86975f4e317e17da9e8bfe05b 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -41,9 +41,14 @@ 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
       (* Status in which the proof could be while it is being processed by the
@@ -74,8 +79,9 @@ let set_metasenv metasenv status =
   let proof_status =
     match status.proof_status with
     | No_proof -> Intermediate metasenv
-    | Incomplete_proof ((uri, _, proof, ty), goal) ->
-        Incomplete_proof ((uri, metasenv, proof, ty), goal)
+    | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) ->
+        Incomplete_proof
+          { incomplete_proof with proof = (uri, metasenv, proof, ty) }
     | Intermediate _ -> Intermediate metasenv 
     | Proof _ -> assert false
   in