X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.mli;h=492bc8c3be3c548c56832ff3862dc98b4ba13f7f;hb=3a12950125e7a4a792546aacea40505f3cecae89;hp=d4de71f019c25f6565d0936693e93de1b173d1a6;hpb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index d4de71f01..492bc8c3b 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -26,19 +26,6 @@ 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 @@ -49,3 +36,11 @@ val time_travel: 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