added set_metasenv on proof_status

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

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