* http://helm.cs.unibo.it/
*)
-val add_constant:
- uri:UriManager.uri ->
- ?body:Cic.term -> ty:Cic.term ->
- ugraph:CicUniv.universe_graph ->
- ?params:UriManager.uri list -> ?attrs:Cic.attribute list ->
+val add_obj:
+ UriManager.uri -> Cic.obj ->
MatitaTypes.status -> MatitaTypes.status
-val add_inductive_def:
- uri:UriManager.uri ->
- types:Cic.inductiveType list ->
- ?params:UriManager.uri list -> ?leftno:int -> ?attrs:Cic.attribute list ->
- ugraph:CicUniv.universe_graph ->
- MatitaTypes.status -> MatitaTypes.status
-
-val add_record_def:
- CicRecord.record_spec ->
- 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.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
+ * @param verbose defaults to false *)
+val remove: ?verbose:bool -> UriManager.uri -> unit