]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaSync.mli
Dead code clean-up.
[helm.git] / helm / matita / matitaSync.mli
index d4de71f019c25f6565d0936693e93de1b173d1a6..fa82d974f0c206eb0738f1363de0ff69d913f217 100644 (file)
 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