X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.mli;h=d5cb663600b3f22f47b5a50606afa43545cada79;hb=210b6e113724900dd5c5745da2881b868154d241;hp=e1a06852704b879455384459b58e9f1f8c220dc4;hpb=b089671a552882bb0666fe6291b339fd5684d523;p=helm.git

diff --git a/matita/components/ng_kernel/nCicExtraction.mli b/matita/components/ng_kernel/nCicExtraction.mli
index e1a068527..d5cb66360 100644
--- a/matita/components/ng_kernel/nCicExtraction.mli
+++ b/matita/components/ng_kernel/nCicExtraction.mli
@@ -11,6 +11,7 @@
 
 (* $Id: nCicEnvironment.mli 11172 2011-01-11 21:06:37Z sacerdot $ *)
 
+type info
 type db
 
 class type g_status =
@@ -26,6 +27,14 @@ class virtual status :
   method set_extraction_status: #g_status -> 'self
  end
 
+val empty_info: info
+
+val refresh_uri_in_info:
+ refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+  info -> info
+
+val register_infos: db -> info -> db
 
 (* Haskell *)
-val haskell_of_obj: (#status as 'status) -> NCic.obj -> 'status * string
+val haskell_of_obj: (#status as 'status) -> NCic.obj ->
+ 'status * (string * info)