From 0b082b38f60079c8d457790c3ee18c2a9ab415eb Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli 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