- (* removes the object from DB, Disk, CoercionsDB, getter
+ (** set the proof aliases enriching the moo_content *)
+val set_proof_aliases :
+ MatitaTypes.status ->
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
+ MatitaTypes.status
+
+ (* removes the object from DB, Disk, CoercionsDB, CicEnvironment, getter