Identity change, improves readability.

[helm.git] / matita / components / ng_kernel / nCicExtraction.mli

diff --git a/matita/components/ng_kernel/nCicExtraction.mli b/matita/components/ng_kernel/nCicExtraction.mli
index b11f38654519d43148e1763eae759f237c181cce..d5cb663600b3f22f47b5a50606afa43545cada79 100644 (file)
--- 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 option
+val haskell_of_obj: (#status as 'status) -> NCic.obj ->
+ 'status * (string * info)