added set_metasenv on proof_status

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 1e5957ae8e91ae7862f84b78e026b209c2510210..3bc1056283d05740630b2d042a859f4d08e2177a 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -66,6 +66,17 @@ type status = {
   notation_ids: CicNotation.notation_id list;
 }
 
+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)
+    | Intermediate _ -> Intermediate metasenv 
+    | Proof _ -> assert false
+  in
+  { status with proof_status = proof_status }
+
 let dump_status status = 
   MatitaLog.message "status.aliases:\n";
   MatitaLog.message