val alias_diff: from:MatitaTypes.status -> MatitaTypes.status ->
DisambiguateTypes.environment
+ (** set the proof aliases enriching the moo_content *)
+val set_proof_aliases :
+ MatitaTypes.status -> DisambiguateTypes.environment -> MatitaTypes.status
+
+ (* removes the object from DB, Disk, CoercionsDB, CicEnvironment, getter
+ * asserts the uri is resolved to file:// so it is only for
+ * user's objects *)
+val remove: verbose:bool -> UriManager.uri -> unit