added set_metasenv on proof_status

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index c36afca247009f7af25cf5a9ad1d76d167f2f031..053f05be6b2b6a70a9e98ff4461030135c2d2087 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -56,6 +56,8 @@ type status = {
   notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
 }
 
+val set_metasenv: Cic.metasenv -> status -> status
+
 val dump_status : status -> unit
 val get_option : status -> StringMap.key -> option_value
 val get_string_option : status -> StringMap.key -> string