let no_options = StringMap.empty
type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
- proof_status: proof_status;
- options: options;
- objects: (UriManager.uri * string) list;
- (** in-scope objects, with their paths *)
+ aliases : DisambiguateTypes.environment;
+ moo_content_rev : string list;
+ proof_status : proof_status;
+ options : options;
+ objects : (UriManager.uri * string) 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 ((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
- (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n");
+ (DisambiguatePp.pp_environment status.aliases ^ "\n");
MatitaLog.message "status.proof_status:";
MatitaLog.message
(match status.proof_status with