From 0b082b38f60079c8d457790c3ee18c2a9ab415eb Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 8 Sep 2005 10:40:16 +0000
Subject: [PATCH] added set_metasenv on proof_status

---
 helm/matita/matitaTypes.ml  | 11 +++++++++++
 helm/matita/matitaTypes.mli |  2 ++
 2 files changed, 13 insertions(+)

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
-- 
2.39.2