]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_library/nCicLibrary.mli
- refreshing of uris in NotationPt.terms implemented
[helm.git] / matita / components / ng_library / nCicLibrary.mli
index b2015a9528f1def60d0f8dc869021dcd9a565520..9f641d1cafc52c758acaaf9a813d42e360650b7c 100644 (file)
@@ -48,6 +48,7 @@ module type SerializerType =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
     refresh_uri_in_term:(NCic.term -> NCic.term) ->
+    refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
      dumpable_status -> dumpable_status
 
   val register: < run: 'a.  string -> 'a register_type -> ('a -> obj) >