Fixes a bug (introduced in the previous revision) which caused the environment

to forget its status.

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index 3bede228d7bafec765e2df7cac49c6527c01535e..9c7ea4768ceb4152cf35839d2cda60fcfb3f90a6 100644 (file)
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -48,6 +48,7 @@ let initial_status = {
 class type g_status =
   object
    inherit Interpretations.g_status
+   inherit NCicLibrary.g_status
    method disambiguate_db: db
   end
 
@@ -63,7 +64,8 @@ class virtual status uid =
             DisambiguateTypes.InterprEnv.empty } >}
   method set_disambiguate_status
    : 'status. #g_status as 'status -> 'self
-      = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
+      = fun o -> ((self#set_interp_status o)#set_disambiguate_db
+      o#disambiguate_db)#set_lib_status o
  end
 
 (* let eval_with_new_aliases status f =

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
index 640f2927009787194fbc4bda0b515e1678c85984..e71c25b828101f2a9e83198a431f3ee21439cff9 100644 (file)
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
@@ -28,6 +28,7 @@ type db
 class type g_status =
  object
   inherit Interpretations.g_status
+  inherit NCicLibrary.g_status
   method disambiguate_db: db
  end
 

diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml
index b775bff001b2e80caab3fb7f8c8785fafaf1c7ec..47a62c048c2bb78ebfd9e5a0cd83f759ebf40069 100644 (file)
--- a/matitaB/components/ng_library/nCicLibrary.ml
+++ b/matitaB/components/ng_library/nCicLibrary.ml
@@ -156,6 +156,7 @@ type db = {
 
 class type g_status =
   object
+    inherit NCicEnvironment.g_status
     method lib_db : db
   end
 
@@ -175,7 +176,7 @@ class virtual status uid =
   method set_timestamp v = {< timestamp = v >}
   method set_lib_db v = {< lib_db = v >}
   method set_lib_status : 's.#g_status as 's -> 'self
-   = fun o -> {< lib_db = o#lib_db >}  
+   = fun o -> {< lib_db = o#lib_db >}#set_env_status o
  end
 
 let reset_timestamp st =

diff --git a/matitaB/components/ng_library/nCicLibrary.mli b/matitaB/components/ng_library/nCicLibrary.mli
index cba90c30cb10e932ba286a93ecbff287cd0e9985..b8453267aaf5522d270ab9561a762bcf99c5218f 100644 (file)
--- a/matitaB/components/ng_library/nCicLibrary.mli
+++ b/matitaB/components/ng_library/nCicLibrary.mli
@@ -20,6 +20,7 @@ type db
 
 class type g_status =
   object
+    inherit NCicEnvironment.g_status
     method lib_db : db
   end