X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.mli;h=ee0c9b6e78fbf1b23447a489ed49f528c3f1a37c;hb=53ee2f5095adadffcafb40e436d23dc330d3bd87;hp=8e85c418617b6b5458340bbc9a0938d350a8a878;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git

diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli
index 8e85c4186..ee0c9b6e7 100644
--- a/helm/matita/matitaSync.mli
+++ b/helm/matita/matitaSync.mli
@@ -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