*)
val add_obj:
- UriManager.uri -> Cic.obj -> MatitaTypes.status -> MatitaTypes.status
+ UriManager.uri -> Cic.obj ->
+ MatitaTypes.status -> MatitaTypes.status
val time_travel:
present:MatitaTypes.status -> past:MatitaTypes.status -> unit
* that the second one can only have more aliases than the first one
* @return the list of aliases that should be added to aliases of from in
* order to be equal to aliases of the second argument *)
-val alias_diff: from:MatitaTypes.status -> MatitaTypes.status ->
- DisambiguateTypes.environment
+val alias_diff:
+ from:MatitaTypes.status -> MatitaTypes.status ->
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list
(** set the proof aliases enriching the moo_content *)
val set_proof_aliases :
- MatitaTypes.status -> DisambiguateTypes.environment -> MatitaTypes.status
+ MatitaTypes.status ->
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
+ 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
+ * user's objects
+ * @param verbose defaults to false *)
+val remove: ?verbose:bool -> UriManager.uri -> unit
+