]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaSync.mli
added records
[helm.git] / helm / matita / matitaSync.mli
index 8e85c418617b6b5458340bbc9a0938d350a8a878..ee0c9b6e78fbf1b23447a489ed49f528c3f1a37c 100644 (file)
@@ -36,6 +36,10 @@ val add_inductive_def:
   ?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