+let dump_status status =
+ MatitaLog.message "status.aliases:\n";
+ MatitaLog.message
+ (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n");
+ MatitaLog.message "status.proof_status:";
+ MatitaLog.message
+ (match status.proof_status with
+ | No_proof -> "no proof\n"
+ | Incomplete_proof _ -> "incomplete proof\n"
+ | Proof _ -> "proof\n"
+ | Intermediate _ -> "Intermediate\n");
+ MatitaLog.message "status.options\n";
+ StringMap.iter (fun k v ->
+ let v =
+ match v with
+ | String s -> s
+ | Int i -> string_of_int i
+ in
+ MatitaLog.message (k ^ "::=" ^ v)) status.options;
+ MatitaLog.message "status.coercions\n";
+ List.iter
+ (fun (u1,u2,u3) -> MatitaLog.message
+ ((UriManager.string_of_uri u1) ^
+ (UriManager.string_of_uri u2) ^
+ (UriManager.string_of_uri u3))) status.coercions;
+ MatitaLog.message "status.objects:\n";
+ List.iter
+ (fun (u,_) ->
+ MatitaLog.message (UriManager.string_of_uri u)) status.objects
+