+type option_value =
+ | String of string
+ | Int of int
+type options = option_value StringMap.t
+let no_options = StringMap.empty
+
+type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list
+
+type status = {
+ aliases: DisambiguateTypes.environment;
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ moo_content_rev: moo;
+ proof_status: proof_status;
+ options: options;
+ objects: (UriManager.uri * string) list;
+ coercions: UriManager.uri list;
+ 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 ({ proof = (uri, _, proof, ty) } as incomplete_proof) ->
+ Incomplete_proof
+ { incomplete_proof with proof = (uri, metasenv, proof, ty) }
+ | Intermediate _ -> Intermediate metasenv
+ | Proof _ -> assert false
+ in
+ { status with proof_status = proof_status }