From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 8 Sep 2005 10:40:16 +0000 (+0000)
Subject: added set_metasenv on proof_status
X-Git-Tag: V_0_1_2_1~58
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0b082b38f60079c8d457790c3ee18c2a9ab415eb;p=helm.git

added set_metasenv on proof_status
---

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 1e5957ae8..3bc105628 100644
--- 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 c36afca24..053f05be6 100644
--- 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