From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 16 Sep 2011 14:14:15 +0000 (+0000)
Subject: This commit patches the environment and the library so that their status is
X-Git-Tag: make_still_working~2277
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e79c8b830f9f6b0c3f4d577909e32e1bb4032cdf;p=helm.git

This commit patches the environment and the library so that their status is
contained in the global status of Matita. This allows several users to execute
concurrently in the same instance of Matita, since they are now using
independent statuses.
---

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index a0b00150f..cbaa4d93a 100644
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -44,7 +44,7 @@ let inject_unification_hint =
    ~alias_only status
  =
   if not alias_only then
-   let t = refresh_uri_in_term (status :> NCic.status) t in
+   let t = refresh_uri_in_term (status :> NCicEnvironment.status) t in
     basic_eval_unification_hint (t,n) status
   else
    status
@@ -152,10 +152,10 @@ let inject_input_notation =
    if not alias_only then
     let l1 =
      CicNotationParser.refresh_uri_in_checked_l1_pattern
-      ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+      ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))
       ~refresh_uri_in_reference l1 in
     let l2 = NotationUtil.refresh_uri_in_term
-      ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+      ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))
       ~refresh_uri_in_reference l2
     in
      basic_eval_input_notation (l1,l2) status
@@ -183,10 +183,10 @@ let inject_output_notation =
   if not alias_only then
    let l1 =
     CicNotationParser.refresh_uri_in_checked_l1_pattern
-     ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+     ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))
       ~refresh_uri_in_reference l1 in
    let l2 = NotationUtil.refresh_uri_in_term
-     ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+     ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))
       ~refresh_uri_in_reference l2
    in
     basic_eval_output_notation (l1,l2) status
@@ -206,7 +206,7 @@ let record_index_obj =
  let aux l ~refresh_uri_in_universe 
    ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status
  =
-  let refresh_uri_in_term = refresh_uri_in_term (status:>NCic.status) in
+  let refresh_uri_in_term = refresh_uri_in_term (status:>NCicEnvironment.status) in
   if not alias_only then
     basic_index_obj
       (List.map 
@@ -322,7 +322,7 @@ let inject_constraint =
     (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment
      * and also to the storage (for undo/redo). During inclusion of compiled
      * files the storage must not be touched. *)
-    NCicEnvironment.add_lt_constraint u1 u2;
+    NCicEnvironment.add_lt_constraint status u1 u2;
     status
   else
    status
@@ -607,7 +607,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                                 let status = status#set_ng_mode `CommandMode in status)
                   status
                   (NCic.Prop::
-                    List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+                    List.map (fun s -> NCic.Type s)
+                    (NCicEnvironment.get_universes status))
               | _ -> status
            in
            let coercions =
diff --git a/matitaB/components/grafite_engine/grafiteTypes.ml b/matitaB/components/grafite_engine/grafiteTypes.ml
index 5b34158c4..f4ec3309c 100644
--- a/matitaB/components/grafite_engine/grafiteTypes.ml
+++ b/matitaB/components/grafite_engine/grafiteTypes.ml
@@ -39,7 +39,7 @@ class virtual status = fun (uid : string option) (b : string) ->
   object
    (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
    inherit ([Continuationals.Stack.t] NTacStatus.status uid fake_obj (Continuationals.Stack.empty))
-   inherit NCicLibrary.dumpable_status
+   inherit NCicLibrary.dumpable_status uid
    inherit NCicLibrary.status uid
    inherit GrafiteDisambiguate.status uid
    inherit GrafiteParser.status uid
diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
index a26d5ec7c..cf3c127b9 100644
--- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
@@ -174,7 +174,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
 let fresh_uri status prefix suffix = 
   let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
   let rec diverge u i =
-    if NCicLibrary.aliases_of u = [] then u
+    if NCicLibrary.aliases_of status u = [] then u
     else diverge (mk ("__" ^ string_of_int i)) (i+1)
   in
    diverge (mk "") 0
@@ -295,7 +295,9 @@ let record_ncoercion =
   ~refresh_uri_in_reference ~alias_only status
  =
   if not alias_only then
-   List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
+   List.fold_right 
+    (aux ~refresh_uri_in_term:(refresh_uri_in_term
+     (status:>NCicEnvironment.status))) l status
   else
    status
  in
diff --git a/matitaB/components/ng_cic_content/ncic2astMatcher.mli b/matitaB/components/ng_cic_content/ncic2astMatcher.mli
index 47721cf4e..50c5e4467 100644
--- a/matitaB/components/ng_cic_content/ncic2astMatcher.mli
+++ b/matitaB/components/ng_cic_content/ncic2astMatcher.mli
@@ -27,7 +27,7 @@ module Matcher32:
 sig
   (** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *)
   val compiler :
-   #NCic.status ->
+   #NCicEnvironment.status ->
     (NotationPt.cic_appl_pattern * int) list ->
       (NCic.term ->
         ((string * NCic.term) list * NCic.term list * int) option)
diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index 4b1bdfcc8..3bede228d 100644
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -54,6 +54,7 @@ class type g_status =
 class virtual status uid =
  object (self)
   inherit Interpretations.status uid
+  inherit NCicLibrary.status uid
   val disambiguate_db = initial_status
   method disambiguate_db = disambiguate_db
   method set_disambiguate_db v = {< disambiguate_db = v >}
@@ -158,13 +159,13 @@ let mk_implicit b =
       GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
 ;;
 
-let nlookup_in_library 
+let nlookup_in_library status
   interactive_user_uri_choice input_or_locate_uri item 
 =
   match item with
   | DisambiguateTypes.Id id -> 
      (try
-       let references = NCicLibrary.resolve id in
+       let references = NCicLibrary.resolve status id in
         List.map
          (fun u -> 
            GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
@@ -295,7 +296,7 @@ let diff_obj loc o1 o2 = match o1,o2 with
 ;;
 
 let disambiguate_nterm status expty context metasenv subst thing
-=
+= 
   let newast, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
@@ -303,7 +304,7 @@ let disambiguate_nterm status expty context metasenv subst thing
         ~aliases:status#disambiguate_db.interpr
         ~expty 
         ~universe:(status#disambiguate_db.multi_aliases)
-        ~lookup_in_library:nlookup_in_library
+        ~lookup_in_library:(nlookup_in_library status)
         ~mk_choice:(ncic_mk_choice status)
         ~mk_implicit ~fix_instance
         ~description_of_alias:GrafiteAst.description_of_alias
@@ -311,7 +312,7 @@ let disambiguate_nterm status expty context metasenv subst thing
   in
   let _,_,thing' = thing in
   let diff = diff_term Stdpp.dummy_loc thing' newast in
-  let status = add_to_interpr status diff
+  let status = add_to_interpr status diff 
   in
    metasenv, subst, status, cic
 ;;
@@ -382,7 +383,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
    singleton "third"
     (NCicDisambiguate.disambiguate_obj
       status
-      ~lookup_in_library:nlookup_in_library
+      ~lookup_in_library:(nlookup_in_library status)
       ~description_of_alias:GrafiteAst.description_of_alias
       ~mk_choice:(ncic_mk_choice status)
       ~mk_implicit ~fix_instance ~uri
@@ -435,7 +436,7 @@ let aliases_for_objs status refs =
  List.concat
   (List.map
     (fun nref ->
-      let references = NCicLibrary.aliases_of nref in
+      let references = NCicLibrary.aliases_of status nref in
        List.map
         (fun u ->
           let name = NCicPp.r2s status true u in
diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
index fcea29e43..640f29270 100644
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
@@ -36,6 +36,7 @@ class virtual status :
  object ('self)
   inherit g_status
   inherit Interpretations.status
+  inherit NCicLibrary.status
   method set_disambiguate_db: db -> 'self
   method reset_disambiguate_db: unit -> 'self
   method set_disambiguate_status: #g_status -> 'self
@@ -57,7 +58,7 @@ val add_to_disambiguation_univ:
   (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status 
 
 val aliases_for_objs:
- #NCic.status -> NUri.uri list ->
+ #NCicLibrary.status -> NUri.uri list ->
   (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
 
 (* args: print function, message (may be empty), status *) 
@@ -81,7 +82,7 @@ type pattern =
   (string * NCic.term) list * NCic.term option
 
 val disambiguate_npattern:
- #NCic.status -> GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
+ #NCicEnvironment.status -> GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
 
 val disambiguate_cic_appl_pattern:
  #status ->
diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
index 6f6bbd1a1..b63f8afaa 100644
--- a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
+++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
@@ -55,4 +55,4 @@ val disambiguate_obj :
    NCic.substitution * NCic.obj)
   list * bool
 
-val disambiguate_path: #NCic.status -> NotationPt.term -> NCic.term
+val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term
diff --git a/matitaB/components/ng_kernel/Makefile b/matitaB/components/ng_kernel/Makefile
index 35b89f3b1..acf7c9728 100644
--- a/matitaB/components/ng_kernel/Makefile
+++ b/matitaB/components/ng_kernel/Makefile
@@ -4,9 +4,9 @@ PREDICATES =
 INTERFACE_FILES = \
 	nUri.mli \
 	nReference.mli \
+	nCicEnvironment.mli \
 	nCicUtils.mli \
 	nCicSubstitution.mli \
-	nCicEnvironment.mli \
 	nCicReduction.mli \
 	nCicTypeChecker.mli \
 	nCicUntrusted.mli \
diff --git a/matitaB/components/ng_kernel/nCicEnvironment.ml b/matitaB/components/ng_kernel/nCicEnvironment.ml
index 1b155a030..d3b6a327c 100644
--- a/matitaB/components/ng_kernel/nCicEnvironment.ml
+++ b/matitaB/components/ng_kernel/nCicEnvironment.ml
@@ -20,13 +20,66 @@ exception BadDependency of string Lazy.t * exn;;
 exception BadConstraint of string Lazy.t;;
 exception AlreadyDefined of string Lazy.t;;
 
-let cache = NUri.UriHash.create 313;;
-let history = ref [];;
-let frozen_list = ref [];;
+type item = 
+  [ `Obj of NUri.uri * NCic.obj 
+  | `Constr of NCic.universe * NCic.universe ]
+;;
+
+type obj_exn =
+  [ `WellTyped of NCic.obj
+  | `Exn of exn ]
+;;
+
+type db = {
+        cache : obj_exn NUri.UriHash.t;
+        history : item list ref;
+        frozen_list : (NUri.uri * NCic.obj) list ref;
+        lt_constraints : (NUri.uri * NUri.uri) list ref;
+        universes : NUri.uri list ref
+}
+
+class type g_status = 
+  object
+  method env_db : db
+  end
+
+
+class virtual status uid =
+ object
+  inherit NCic.status uid
+
+  val db = { 
+    cache = NUri.UriHash.create 313;
+    history = ref [];
+    frozen_list = ref [];
+    lt_constraints = ref []; (* a,b := a < b *)
+    universes = ref []
+  }
+
+  method env_db = db
+
+  method set_env_db v = {< db = v >}
+  method set_env_status : 's.#g_status as 's -> 'self
+   = fun o -> {< db = o#env_db >}
+ end
+;;
+
+let get_obj = ref (fun _ _ -> assert false);;
 
-let get_obj = ref (fun _ _ -> assert false) ;;
 let set_get_obj = (:=) get_obj;;
 
+let typechk_already_set = ref false;;  
+let typecheck_obj = ref (fun _ _ -> assert false);;
+
+let set_typecheck_obj f = 
+  if !typechk_already_set then
+   assert false
+  else
+   begin
+    typecheck_obj := f;
+    typechk_already_set := true
+   end
+
 module F = Format 
 
 let rec ppsort f = function
@@ -68,19 +121,17 @@ let max (l1:NCic.universe) (l2:NCic.universe) =
      | (`CProp, u)::tl -> (`Type, u)::tl
 ;;
 
-let lt_constraints = ref [] (* a,b := a < b *)
-
-let rec lt_path_uri avoid a b = 
+let rec lt_path_uri s avoid a b = 
  List.exists
   (fun (x,y) ->
       NUri.eq y b && 
      (NUri.eq a x ||
         (not (List.exists (NUri.eq x) avoid) &&
-        lt_path_uri (x::avoid) a x))
-  ) !lt_constraints
+        lt_path_uri s (x::avoid) a x))
+  ) !(s#env_db.lt_constraints)
 ;;
 
-let lt_path a b = lt_path_uri [b] a b;;
+let lt_path s a b = lt_path_uri s [b] a b;;
 
 let universe_eq a b = 
   match a,b with 
@@ -93,23 +144,23 @@ let universe_eq a b =
       (lazy "trying to check if two inferred universes are equal"))
 ;;
 
-let universe_leq a b = 
+let universe_leq s a b = 
   match a, b with
   | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
   | l, [((`Type|`CProp),b)] -> 
        List.for_all 
          (function 
-         | `Succ,a -> lt_path a b 
-         | _, a -> NUri.eq a b || lt_path a b) l
+         | `Succ,a -> lt_path s a b 
+         | _, a -> NUri.eq a b || lt_path s a b) l
   | _, ([] | [`Succ,_] | _::_::_) -> 
      raise (BadConstraint (lazy (
        "trying to check if "^string_of_univ a^
        " is leq than the inferred universe " ^ string_of_univ b)))
 ;;
 
-let are_sorts_convertible ~test_eq_only s1 s2 =
+let are_sorts_convertible st ~test_eq_only s1 s2 =
    match s1,s2 with
-   | C.Type a, C.Type b when not test_eq_only -> universe_leq a b
+   | C.Type a, C.Type b when not test_eq_only -> universe_leq st a b
    | C.Type a, C.Type b -> universe_eq a b
    | C.Prop,C.Type _ -> (not test_eq_only)
    | C.Prop, C.Prop -> true
@@ -120,31 +171,30 @@ let pp_constraint x y =
   NUri.name_of_uri x ^ " < " ^ NUri.name_of_uri y
 ;;
 
-let pp_constraints () =
-  String.concat "\n" (List.map (fun (x,y) -> pp_constraint x y) !lt_constraints)
+let pp_constraints s =
+  String.concat "\n" (List.map (fun (x,y) -> pp_constraint x y)
+   !(s#env_db.lt_constraints))
 ;;
 
-let universes = ref [];;
-
-let get_universes () = 
-  List.map (fun x -> [`Type,x]) !universes @
-  List.map (fun x -> [`CProp,x]) !universes
+let get_universes s = 
+  List.map (fun x -> [`Type,x]) !(s#env_db.universes) @
+  List.map (fun x -> [`CProp,x]) !(s#env_db.universes)
 ;;
 
-let is_declared u =
+let is_declared s u =
  match u with
- | [(`CProp|`Type),x] -> List.exists (fun y -> NUri.eq x y) !universes
+ | [(`CProp|`Type),x] -> List.exists (fun y -> NUri.eq x y) !(s#env_db.universes)
  | _ -> assert false
 ;;
 
 exception UntypableSort of string Lazy.t
 exception AssertFailure of string Lazy.t
 
-let typeof_sort = function
+let typeof_sort s = function
   | C.Type ([(`Type|`CProp),u] as univ) ->
-     if is_declared univ then (C.Type [`Succ, u])
+     if is_declared s univ then (C.Type [`Succ, u])
      else 
-      let universes = !universes in
+      let universes = !(s#env_db.universes) in
        raise (UntypableSort (lazy ("undeclared universe " ^
          NUri.string_of_uri u ^ "\ndeclared ones are: " ^ 
          String.concat ", " (List.map NUri.string_of_uri universes)
@@ -155,76 +205,77 @@ let typeof_sort = function
   | C.Prop -> (C.Type [])
 ;;
 
-let add_lt_constraint a b = 
+let add_lt_constraint s a b = 
   match a,b with
   | [`Type,a2],[`Type,b2] -> 
-      if not (lt_path_uri [] a2 b2) then (
-        if lt_path_uri [] b2 a2 || NUri.eq a2 b2 then
+      if not (lt_path_uri s [] a2 b2) then (
+        if lt_path_uri s [] b2 a2 || NUri.eq a2 b2 then
          (raise(BadConstraint(lazy("universe inconsistency adding "^
                     pp_constraint a2 b2
-           ^ " to:\n" ^ pp_constraints ()))));
-        universes := a2 :: b2 :: 
-          List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes;
-        lt_constraints := (a2,b2) :: !lt_constraints);
-      history := (`Constr (a,b))::!history;
+           ^ " to:\n" ^ pp_constraints s))));
+        s#env_db.universes := a2 :: b2 :: 
+          List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2))
+          !(s#env_db.universes);
+        s#env_db.lt_constraints := (a2,b2) :: !(s#env_db.lt_constraints));
+        s#env_db.history := (`Constr (a,b))::!(s#env_db.history);
   | _ -> raise (BadConstraint
-          (lazy "trying to add a constraint on an inferred universe"))
+          (lazy "trying to add a constraint on an inferred universe"));
 ;;
    
 let family_of = function (`CProp,_)::_ -> `CProp | _ -> `Type ;;
 
-let sup fam l =
+let sup s fam l =
   match l with
   | [(`Type|`CProp),_] -> Some l
   | l ->
    let bigger_than acc (s1,n1) = 
     List.filter
-     (fun x -> lt_path_uri [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc 
+     (fun x -> lt_path_uri s [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc 
    in
-   let solutions = List.fold_left bigger_than !universes l in
+   let solutions = List.fold_left bigger_than !(s#env_db.universes) l in
    let rec aux = function
      | [] -> None
      | u :: tl ->
-         if List.exists (fun x -> lt_path_uri [] x u) solutions then aux tl
+         if List.exists (fun x -> lt_path_uri s [] x u) solutions then aux tl
          else Some [fam,u]
    in
     aux solutions
 ;;
 
-let sup l = sup (family_of l) l;;
+let sup s l = sup s (family_of l) l;;
 
-let inf ~strict fam l =
+let inf s ~strict fam l =
   match l with
   | [(`Type|`CProp),_] -> Some l
   | [] -> None
   | l ->
    let smaller_than acc (_s1,n1) = 
     List.filter
-     (fun x -> lt_path_uri [] x n1 || (not strict && NUri.eq n1 x)) acc 
+     (fun x -> lt_path_uri s [] x n1 || (not strict && NUri.eq n1 x)) acc 
    in
-   let solutions = List.fold_left smaller_than !universes l in
+   let solutions = List.fold_left smaller_than !(s#env_db.universes) l in
    let rec aux = function
      | [] -> None
      | u :: tl ->
-         if List.exists (lt_path_uri [] u) solutions then aux tl
+         if List.exists (lt_path_uri s [] u) solutions then aux tl
          else Some [fam,u]
    in
     aux solutions
 ;;
 
-let inf ~strict l = inf ~strict (family_of l) l;;
+let inf s ~strict l = inf s ~strict (family_of l) l;;
 
-let rec universe_lt a b = 
+let rec universe_lt s a b = 
   match a, b with
   | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
   | l, ([((`Type|`CProp),b)] as orig_b) -> 
        List.for_all 
          (function 
          | `Succ,_ as a -> 
-             (match sup [a] with
+             (match sup s [a] with
              | None -> false
-             | Some x -> universe_lt x orig_b) 
-         | _, a -> lt_path a b) l
+             | Some x -> universe_lt s x orig_b) 
+         | _, a -> lt_path s a b) l
   | _, ([] | [`Succ,_] | _::_::_) -> 
      raise (BadConstraint (lazy (
        "trying to check if "^string_of_univ a^
@@ -243,17 +294,6 @@ let allowed_sort_elimination s1 s2 =
   | C.Prop, C.Type _ -> `UnitOnly
 ;;
 
-let typecheck_obj,already_set = ref (fun _ _ -> assert false), ref false;;
-let set_typecheck_obj f =
- if !already_set then
-  assert false
- else
-  begin
-   typecheck_obj := f;
-   already_set := true
-  end
-;;
-
 (* CSC: old code that performs recursive invalidation; to be removed
  * once we understand what we really want. Once we removed it, we can
  * also remove the !history
@@ -284,13 +324,13 @@ let invalidate_item item =
 ;;
 *)
 
-let invalidate_item =
- function
-    `Obj (uri,_) -> NUri.UriHash.remove cache uri
+let invalidate_item s o =
+  match o with
+  | `Obj (uri,_) -> NUri.UriHash.remove s#env_db.cache uri
   | `Constr ([_,u1],[_,u2]) -> 
       let w = u1,u2 in
-      lt_constraints := List.filter ((<>) w) !lt_constraints;
-  | `Constr _ -> assert false
+      s#env_db.lt_constraints := List.filter ((<>) w) !(s#env_db.lt_constraints);
+  | `Constr _ -> assert false;
 ;;
 
 exception Propagate of NUri.uri * exn;;
@@ -301,57 +341,59 @@ let to_exn f x =
   | `Exn e -> raise e
 ;;
 
-let check_and_add_obj (status:#NCic.status) ((u,_,_,_,_) as obj) =
- let saved_frozen_list = !frozen_list in
+let check_and_add_obj (status:#status) ((u,_,_,_,_) as obj) =
+ let saved_frozen_list = !(status#env_db.frozen_list) in
  try
-   frozen_list := (u,obj)::saved_frozen_list;
-   HLog.warn ("Typechecking of " ^ NUri.string_of_uri u); 
-   !typecheck_obj (status :> NCic.status) obj;
-   frozen_list := saved_frozen_list;
+   status#env_db.frozen_list := (u,obj)::saved_frozen_list;
+   HLog.warn ("Typechecking of " ^ NUri.string_of_uri u);
+   !typecheck_obj (status :> status) obj;
+   status#env_db.frozen_list := saved_frozen_list;
    let obj' = `WellTyped obj in
-   NUri.UriHash.add cache u obj';
-   history := (`Obj (u,obj))::!history;
+   NUri.UriHash.add status#env_db.cache u obj';
+   status#env_db.history := (`Obj (u,obj))::!(status#env_db.history);
    obj'
  with
     Sys.Break as e ->
-     frozen_list := saved_frozen_list;
+     status#env_db.frozen_list := saved_frozen_list;
      raise e
   | Propagate (u',old_exn) as e' ->
-     frozen_list := saved_frozen_list;
+     status#env_db.frozen_list := saved_frozen_list;
      let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
        " depends (recursively) on " ^ NUri.string_of_uri u' ^
        " which is not well-typed"), 
        match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in
-     NUri.UriHash.add cache u exn;
-     history := (`Obj (u,obj))::!history;
+     NUri.UriHash.add status#env_db.cache u exn;
+     status#env_db.history := (`Obj (u,obj))::!(status#env_db.history);
      if saved_frozen_list = [] then
       exn
      else
       raise e'
   | e ->
-     frozen_list := saved_frozen_list;
+     status#env_db.frozen_list := saved_frozen_list;
      let exn = `Exn e in
-     NUri.UriHash.add cache u exn;
-     history := (`Obj (u,obj))::!history;
+     NUri.UriHash.add status#env_db.cache u exn;
+     status#env_db.history := (`Obj (u,obj))::!(status#env_db.history);
      if saved_frozen_list = [] then
       exn
      else
       raise (Propagate (u,e))
 ;;
 
-let get_checked_obj status u =
- if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
+let get_checked_obj (status:#status) u =
+ if List.exists (fun (k,_) -> NUri.eq u k) !(status#env_db.frozen_list)
  then
   raise (CircularDependency (lazy (NUri.string_of_uri u)))
  else
-  try NUri.UriHash.find cache u
-  with Not_found -> check_and_add_obj status (!get_obj (status :> NCic.status) u)
+  try NUri.UriHash.find status#env_db.cache u
+  with Not_found -> 
+    (* XXX: to be checked carefully *)
+    check_and_add_obj status (!get_obj (status :> status) u)
 ;;
 
-let get_checked_obj (status:#NCic.status) u = to_exn (get_checked_obj status) u;;
+let get_checked_obj status u = to_exn (get_checked_obj status) u;;
 
 let check_and_add_obj status ((u,_,_,_,_) as obj) =
- if NUri.UriHash.mem cache u then
+ if NUri.UriHash.mem status#env_db.cache u then
   raise (AlreadyDefined (lazy (NUri.string_of_uri u)))
  else
   ignore (to_exn (check_and_add_obj status) obj)
@@ -418,7 +460,7 @@ let get_relevance status (Ref.Ref (_, infos) as r) =
 ;;
 
 
-let invalidate _ = 
-  assert (!frozen_list = []);
-  NUri.UriHash.clear cache
+let invalidate s = 
+  assert (!(s#env_db.frozen_list) = []);
+  NUri.UriHash.clear s#env_db.cache
 ;;
diff --git a/matitaB/components/ng_kernel/nCicEnvironment.mli b/matitaB/components/ng_kernel/nCicEnvironment.mli
index 80fcd2b68..790d72abe 100644
--- a/matitaB/components/ng_kernel/nCicEnvironment.mli
+++ b/matitaB/components/ng_kernel/nCicEnvironment.mli
@@ -16,41 +16,66 @@ exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t * exn;;
 exception AlreadyDefined of string Lazy.t;;
 
-val set_get_obj: (NCic.status -> NUri.uri -> NCic.obj) -> unit
+type item = 
+  [ `Obj of NUri.uri * NCic.obj 
+  | `Constr of NCic.universe * NCic.universe ]
+;;
 
-val get_checked_obj: #NCic.status -> NUri.uri -> NCic.obj
+type obj_exn =
+  [ `WellTyped of NCic.obj
+  | `Exn of exn ]
+;;
 
-val check_and_add_obj: #NCic.status -> NCic.obj -> unit
+type db
 
-val get_relevance: #NCic.status -> NReference.reference -> bool list
+class type g_status = 
+  object
+    method env_db : db
+  end
+
+class virtual status : string option ->
+ object('self)
+  inherit NCic.status
+  inherit g_status
+  method set_env_db : db -> 'self
+  method set_env_status : #g_status -> 'self
+ end
+
+val set_get_obj : (status -> NUri.uri -> NCic.obj) -> unit
+val set_typecheck_obj : (status -> NCic.obj -> unit) -> unit
+
+val get_checked_obj: #status -> NUri.uri -> NCic.obj
+
+val check_and_add_obj: #status -> NCic.obj -> unit
+
+val get_relevance: #status -> NReference.reference -> bool list
 
 val get_checked_def:
-  #NCic.status -> NReference.reference -> 
+    #status -> NReference.reference -> 
     NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int
 
 (* the last integer is the index of the inductive type in the reference *)
 val get_checked_indtys:
-  #NCic.status -> NReference.reference -> 
+    #status -> NReference.reference -> 
     bool * int * NCic.inductiveType list * NCic.i_attr * int
 
 val get_checked_fixes_or_cofixes:
-  #NCic.status -> NReference.reference -> 
+   #status -> NReference.reference -> 
    NCic.inductiveFun list * NCic.f_attr * int
 
-val invalidate_item: 
+val invalidate_item:
+      #status -> 
       [ `Obj of NUri.uri * NCic.obj 
       | `Constr of NCic.universe * NCic.universe ] -> unit
 
-val invalidate: unit -> unit
-
-val set_typecheck_obj: (NCic.status -> NCic.obj -> unit) -> unit
+val invalidate: #status -> unit
 
 (* =========== universes ============= *)
 
 (* utils *)
 val ppsort : Format.formatter -> NCic.sort -> unit
-val pp_constraints: unit -> string
-val get_universes: unit -> NCic.universe list
+val pp_constraints: #status -> string
+val get_universes: #status -> NCic.universe list
 
 (* use to type products *)
 val max: NCic.universe -> NCic.universe -> NCic.universe
@@ -58,13 +83,13 @@ val max: NCic.universe -> NCic.universe -> NCic.universe
 (* raise BadConstraints if the second arg. is an inferred universe or
  * if the added constraint gives circularity *)
 exception BadConstraint of string Lazy.t;;
-val add_lt_constraint: NCic.universe -> NCic.universe -> unit
+val add_lt_constraint: #status -> NCic.universe -> NCic.universe -> unit
 val universe_eq: NCic.universe -> NCic.universe -> bool
-val universe_leq: NCic.universe -> NCic.universe -> bool
-val universe_lt: NCic.universe -> NCic.universe -> bool
+val universe_leq: #status -> NCic.universe -> NCic.universe -> bool
+val universe_lt: #status -> NCic.universe -> NCic.universe -> bool
 
 (* checks if s1 <= s2 *)
-val are_sorts_convertible: test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
+val are_sorts_convertible: #status -> test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
 
 (* to type a Match *)
 val allowed_sort_elimination: NCic.sort -> NCic.sort -> [ `Yes | `UnitOnly ]
@@ -72,11 +97,11 @@ val allowed_sort_elimination: NCic.sort -> NCic.sort -> [ `Yes | `UnitOnly ]
 (* algebraic successor function *)
 exception UntypableSort of string Lazy.t
 exception AssertFailure of string Lazy.t
-val typeof_sort: NCic.sort -> NCic.sort
+val typeof_sort: #status -> NCic.sort -> NCic.sort
 
 (* looks for a declared universe that is the least one above the input *)
-val sup : NCic.universe -> NCic.universe option
-val inf : strict:bool -> NCic.universe -> NCic.universe option
+val sup : #status -> NCic.universe -> NCic.universe option
+val inf : #status -> strict:bool -> NCic.universe -> NCic.universe option
 val family_of : NCic.universe -> [ `CProp | `Type ]
 
 (* =========== /universes ============= *)
diff --git a/matitaB/components/ng_kernel/nCicPp.ml b/matitaB/components/ng_kernel/nCicPp.ml
index 84c95f45a..80eb372ae 100644
--- a/matitaB/components/ng_kernel/nCicPp.ml
+++ b/matitaB/components/ng_kernel/nCicPp.ml
@@ -141,7 +141,7 @@ let ppterm status ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t
       let _,_,t,_ = List.assoc n subst in
       let hd = NCicSubstitution.subst_meta status lc t in
       aux ctx 
-        (NCicReduction.head_beta_reduce (status :> NCic.status) ~upto:(List.length args)
+        (NCicReduction.head_beta_reduce (status :> NCicEnvironment.status) ~upto:(List.length args)
           (match hd with
           | NCic.Appl l -> NCic.Appl (l@args)
           | _ -> NCic.Appl (hd :: args)))
@@ -359,8 +359,15 @@ let ppsubst status ~metasenv ?use_subst subst =
 
 let ppobj status obj = on_buffer (ppobj status) obj;;
 
+class type cstatus =
+  object
+    inherit NCicEnvironment.status
+    inherit NCic.cstatus
+  end
+
 class status (uid : string option) =
  object(self)
+  inherit NCicEnvironment.status uid
   (* this method is meant to be overridden in ApplyTransformation *)
   method user = uid
   method ppterm = ppterm self
diff --git a/matitaB/components/ng_kernel/nCicPp.mli b/matitaB/components/ng_kernel/nCicPp.mli
index 06be5b261..fcaa9d199 100644
--- a/matitaB/components/ng_kernel/nCicPp.mli
+++ b/matitaB/components/ng_kernel/nCicPp.mli
@@ -11,13 +11,19 @@
 
 (* $Id$ *)
 
-val r2s: #NCic.status -> bool -> NReference.reference -> string
+val r2s: #NCicEnvironment.status -> bool -> NReference.reference -> string
 
 val string_of_flavour: NCic.def_flavour -> string
 
+class type cstatus =
+  object
+    inherit NCicEnvironment.status
+    inherit NCic.cstatus
+  end
+
 (* low-level pretty printer;
    all methods are meant to be overridden in ApplyTransformation *)
-class status: string option -> NCic.cstatus
+class status: string option -> cstatus
 
 (* variants that use a formatter 
 module Format : sig
diff --git a/matitaB/components/ng_kernel/nCicReduction.ml b/matitaB/components/ng_kernel/nCicReduction.ml
index 8a84810a3..4fd42aa28 100644
--- a/matitaB/components/ng_kernel/nCicReduction.ml
+++ b/matitaB/components/ng_kernel/nCicReduction.ml
@@ -208,18 +208,18 @@ let whd = R.whd
 
 let (===) x y = Pervasives.compare x y = 0 ;;
 
-let get_relevance = ref (fun _ ~metasenv:_ ~subst:_ _ _ -> assert false);;
+let get_relevance = ref (fun (_:#NCicEnvironment.status) ~metasenv:_ ~subst:_ _ _ -> assert false);;
 
 let set_get_relevance = (:=) get_relevance;;
 
-let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv subst context
+let alpha_eq (status:#NCicEnvironment.status) ~test_lambda_source aux test_eq_only metasenv subst context
  t1 t2 =
  if t1 === t2 then
    true
  else
    match (t1,t2) with
    | C.Sort s1, C.Sort s2 -> 
-       NCicEnvironment.are_sorts_convertible ~test_eq_only s1 s2 
+       NCicEnvironment.are_sorts_convertible status ~test_eq_only s1 s2 
 
    | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
        aux true context s1 s2 &&
@@ -285,7 +285,7 @@ let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv
         with Invalid_argument _ -> false
            | HExtlib.FailureAt fail ->
              let relevance = 
-               !get_relevance (status :> NCic.status) ~metasenv ~subst context hd1 tl1 in
+               !get_relevance (status :> NCicEnvironment.status) ~metasenv ~subst context hd1 tl1 in
              let _,relevance = HExtlib.split_nth fail relevance in
              let b,relevance = (match relevance with
                | [] -> assert false
@@ -302,7 +302,7 @@ let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv
 
    | (C.Appl (hd1::tl1),  C.Appl (hd2::tl2)) ->
        aux test_eq_only context hd1 hd2 &&
-        let relevance = !get_relevance (status :> NCic.status) ~metasenv ~subst context hd1 tl1 in
+        let relevance = !get_relevance (status :> NCicEnvironment.status) ~metasenv ~subst context hd1 tl1 in
         (try
          HExtlib.list_forall_default3
           (fun t1 t2 b -> not b || aux true context t1 t2)
diff --git a/matitaB/components/ng_kernel/nCicReduction.mli b/matitaB/components/ng_kernel/nCicReduction.mli
index f53cb5dc8..afe09ddae 100644
--- a/matitaB/components/ng_kernel/nCicReduction.mli
+++ b/matitaB/components/ng_kernel/nCicReduction.mli
@@ -16,15 +16,15 @@ exception AssertFailure of string Lazy.t;;
 val debug: bool ref
 
 val whd : 
-  #NCic.status -> ?delta:int -> subst:NCic.substitution -> 
+  #NCicEnvironment.status -> ?delta:int -> subst:NCic.substitution -> 
   NCic.context -> NCic.term -> NCic.term
 
 val set_get_relevance : 
-  (NCic.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
+  (NCicEnvironment.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
    NCic.context -> NCic.term -> NCic.term list -> bool list) -> unit
 
 val are_convertible :
-  #NCic.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
+  #NCicEnvironment.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
   NCic.context -> NCic.term -> NCic.term -> bool
 
 
@@ -32,7 +32,7 @@ val are_convertible :
    delta reduction; if provided, ~upto is the maximum number of beta redexes
    reduced *)
 val head_beta_reduce: 
- #NCic.status -> ?delta:int -> ?upto:int -> ?subst:NCic.substitution ->
+  #NCicEnvironment.status -> ?delta:int -> ?upto:int -> ?subst:NCic.substitution ->
   NCic.term -> NCic.term
 
 type stack_item
@@ -41,17 +41,17 @@ type environment_item
 type machine = int * environment_item list * NCic.term * stack_item list
 
 val reduce_machine : 
- #NCic.status -> delta:int -> ?subst:NCic.substitution -> NCic.context ->
+ #NCicEnvironment.status -> delta:int -> ?subst:NCic.substitution -> NCic.context ->
   machine -> machine * bool
 val from_stack : delta:int -> stack_item -> machine
 val from_env : delta:int -> environment_item -> machine
-val unwind : #NCic.status -> machine -> NCic.term
+val unwind : #NCicEnvironment.status -> machine -> NCic.term
 
 val split_prods:
- #NCic.status -> subst:NCic.substitution -> NCic.context -> int -> NCic.term ->
+ #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> int -> NCic.term ->
   NCic.context * NCic.term
 
 (* to be used outside the kernel *)
 val alpha_eq:
- #NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
+ #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
   NCic.term -> NCic.term -> bool
diff --git a/matitaB/components/ng_kernel/nCicSubstitution.mli b/matitaB/components/ng_kernel/nCicSubstitution.mli
index 9ba2d11fa..8db93d0c0 100644
--- a/matitaB/components/ng_kernel/nCicSubstitution.mli
+++ b/matitaB/components/ng_kernel/nCicSubstitution.mli
@@ -11,14 +11,14 @@
 
 (* $Id$ *)
 
-val lift_from : #NCic.status -> ?no_implicit:bool -> int -> int -> NCic.term -> NCic.term 
+val lift_from : #NCicEnvironment.status -> ?no_implicit:bool -> int -> int -> NCic.term -> NCic.term 
 
 (* lift n t                                                              *)
 (*  lifts [t] of [n]                                                     *)
 (*  [from] default 1, lifts only indexes >= [from]                       *)
 (*  NOTE: the opposite function (delift_rels) is defined in CicMetaSubst *)
 (*  since it needs to restrict the metavariables in case of failure      *)
-val lift : #NCic.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term
+val lift : #NCicEnvironment.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term
 
 (* subst t1 t2                                                          *)
 (*  substitutes [t1] for [Rel 1] in [t2]                                *)
@@ -26,7 +26,7 @@ val lift : #NCic.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term ->
 (*  are generated. WARNING: the substitution can diverge when t2 is not *)
 (*  well typed and avoid_beta_redexes is true.                          *)
 val subst : 
-  #NCic.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool -> 
+  #NCicEnvironment.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool -> 
   NCic.term -> NCic.term -> NCic.term
 
 (* psubst [avoid] [map_arg] [args] [t]            
@@ -37,7 +37,7 @@ val subst :
  *    the function is ReductionStrategy.from_env_for_unwind when psubst is
  *    used to implement nCicReduction.unwind'                              *)
 val psubst : 
-  #NCic.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool ->
+  #NCicEnvironment.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool ->
   ('a -> NCic.term) -> 'a list -> NCic.term -> 
     NCic.term
 
@@ -45,5 +45,5 @@ val psubst :
 (*  returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *)
 (*  [t_i] is lifted as usual when it crosses an abstraction                  *)
 (* subst_meta (n, Irl _) t -> lift n t                                        *)
-val subst_meta : #NCic.status -> NCic.local_context -> NCic.term -> NCic.term
+val subst_meta : #NCicEnvironment.status -> NCic.local_context -> NCic.term -> NCic.term
 
diff --git a/matitaB/components/ng_kernel/nCicTypeChecker.ml b/matitaB/components/ng_kernel/nCicTypeChecker.ml
index 0a73358e0..489b89287 100644
--- a/matitaB/components/ng_kernel/nCicTypeChecker.ml
+++ b/matitaB/components/ng_kernel/nCicTypeChecker.ml
@@ -382,7 +382,7 @@ let type_of_branch (status:#NCic.status) ~subst context leftno outty cons tycons
 ;;
 
 
-let rec typeof (status:#NCic.status) ~subst ~metasenv context term =
+let rec typeof (status:#NCicEnvironment.status) ~subst ~metasenv context term =
   let rec typeof_aux context = 
     fun t -> (*prerr_endline (status#ppterm ~metasenv ~subst ~context t);*)
     match t with
@@ -395,7 +395,7 @@ let rec typeof (status:#NCic.status) ~subst ~metasenv context term =
           raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
             ^" under: " ^ status#ppcontext ~metasenv ~subst context))))
     | C.Sort s -> 
-         (try C.Sort (NCicEnvironment.typeof_sort s) 
+         (try C.Sort (NCicEnvironment.typeof_sort status s) 
          with 
          | NCicEnvironment.UntypableSort msg -> raise (TypeCheckerFailure msg)
          | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
@@ -793,7 +793,7 @@ and check_mutual_inductive_defs status uri ~metasenv ~subst leftno tyl =
            let con_sort = typeof status ~subst ~metasenv context te in
            (match R.whd status ~subst context con_sort, R.whd status ~subst [] ty_sort with
                (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
-                if not (E.universe_leq u1 u2) then
+                if not (E.universe_leq status u1 u2) then
                  raise
                   (TypeCheckerFailure
                     (lazy ("The type " ^ status#ppterm ~metasenv ~subst ~context s1^
@@ -1114,7 +1114,7 @@ and type_of_constant status ((Ref.Ref (uri,_)) as ref) =
      (lazy ("type_of_constant: environment/reference: " ^
        Ref.string_of_reference ref)))
 
-and get_relevance status ~metasenv ~subst context t args = 
+and get_relevance (status:#NCicEnvironment.status) ~metasenv ~subst context t args = 
    let ty = typeof status ~subst ~metasenv context t in
    let rec aux context ty = function
      | [] -> [] 
diff --git a/matitaB/components/ng_kernel/nCicTypeChecker.mli b/matitaB/components/ng_kernel/nCicTypeChecker.mli
index 6ca329fbf..cbbc770f0 100644
--- a/matitaB/components/ng_kernel/nCicTypeChecker.mli
+++ b/matitaB/components/ng_kernel/nCicTypeChecker.mli
@@ -26,21 +26,21 @@ val set_logger:
 val set_trust : (NCic.obj -> bool) -> unit
 
 val typeof: 
- #NCic.status -> subst:NCic.substitution -> metasenv:NCic.metasenv -> 
+  #NCicEnvironment.status -> subst:NCic.substitution -> metasenv:NCic.metasenv -> 
   NCic.context -> NCic.term -> NCic.term
 
 val height_of_obj_kind:
- #NCic.status -> NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int
+ #NCicEnvironment.status -> NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int
 
 val get_relevance : 
- #NCic.status ->
+ #NCicEnvironment.status ->
   metasenv:NCic.metasenv -> subst:NCic.substitution ->
   NCic.context -> NCic.term -> NCic.term list -> bool list
 
 (* type_of_branch subst context leftno outtype 
  *   (constr @ lefts) (ty_constr @ lefts)  *)
 val type_of_branch : 
- #NCic.status ->
+ #NCicEnvironment.status ->
   subst:NCic.substitution ->
     NCic.context -> int -> NCic.term -> NCic.term -> NCic.term -> 
      NCic.term
@@ -49,7 +49,7 @@ val type_of_branch :
  * arity1 = constructor type @ lefts
  * arity2 = outtype *)
 val check_allowed_sort_elimination : 
- #NCic.status ->
+ #NCicEnvironment.status ->
   subst:NCic.substitution ->
   metasenv:NCic.metasenv ->
   NReference.reference -> NCic.context -> 
@@ -57,13 +57,13 @@ val check_allowed_sort_elimination :
 
 (* Functions to be used by the refiner *)
 val debruijn:
- #NCic.status -> NUri.uri -> int -> subst:NCic.substitution -> NCic.context ->
+ #NCicEnvironment.status -> NUri.uri -> int -> subst:NCic.substitution -> NCic.context ->
   NCic.term -> NCic.term
 
 val are_all_occurrences_positive: 
- #NCic.status -> subst:NCic.substitution -> NCic.context -> NUri.uri -> int ->
+ #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> NUri.uri -> int ->
   int -> int -> int -> NCic.term -> bool
 
 val does_not_occur :
- #NCic.status -> subst:NCic.substitution -> NCic.context -> int -> int ->
+ #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> int -> int ->
   NCic.term -> bool
diff --git a/matitaB/components/ng_kernel/nCicUntrusted.mli b/matitaB/components/ng_kernel/nCicUntrusted.mli
index 7967936e3..b085be307 100644
--- a/matitaB/components/ng_kernel/nCicUntrusted.mli
+++ b/matitaB/components/ng_kernel/nCicUntrusted.mli
@@ -12,7 +12,7 @@
 (* $Id$ *)
 
 val map_term_fold_a:
- #NCic.status ->
+ #NCicEnvironment.status ->
  (NCic.hypothesis -> 'k -> 'k) -> 'k ->
  ('k -> 'a -> NCic.term -> 'a * NCic.term) -> 'a -> NCic.term -> 'a * NCic.term
 
@@ -20,9 +20,9 @@ val map_obj_kind:
   ?skip_body:bool -> (NCic.term -> NCic.term) -> NCic.obj_kind -> NCic.obj_kind
 
 val metas_of_term :
- #NCic.status -> NCic.substitution -> NCic.context -> NCic.term -> int list
+ #NCicEnvironment.status -> NCic.substitution -> NCic.context -> NCic.term -> int list
 val sort_metasenv:
- #NCic.status -> NCic.substitution -> NCic.metasenv -> NCic.metasenv
+ #NCicEnvironment.status -> NCic.substitution -> NCic.metasenv -> NCic.metasenv
 
 type meta_kind = [ `IsSort | `IsType | `IsTerm ]
 val kind_of_meta: NCic.meta_attrs -> meta_kind
@@ -40,14 +40,14 @@ val mk_appl : NCic.term -> NCic.term list -> NCic.term
 
 (* the context is needed only to honour Barendregt's naming convention *)
 val apply_subst :
- #NCic.status -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term
+ #NCicEnvironment.status -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term
 val apply_subst_context :
- #NCic.status -> fix_projections:bool -> 
+ #NCicEnvironment.status -> fix_projections:bool -> 
   NCic.substitution -> NCic.context -> NCic.context
 val apply_subst_metasenv :
- #NCic.status -> NCic.substitution -> NCic.metasenv -> NCic.metasenv
+ #NCicEnvironment.status -> NCic.substitution -> NCic.metasenv -> NCic.metasenv
 
 val count_occurrences :
- #NCic.status -> subst:NCic.substitution -> int -> NCic.term -> int
+ #NCicEnvironment.status -> subst:NCic.substitution -> int -> NCic.term -> int
 (* quick, but with false negatives (since no ~subst), check for closed terms *)
 val looks_closed : NCic.term -> bool
diff --git a/matitaB/components/ng_kernel/nCicUtils.ml b/matitaB/components/ng_kernel/nCicUtils.ml
index f22e02a7e..400d69363 100644
--- a/matitaB/components/ng_kernel/nCicUtils.ml
+++ b/matitaB/components/ng_kernel/nCicUtils.ml
@@ -17,7 +17,7 @@ module Ref = NReference
 exception Subst_not_found of int
 exception Meta_not_found of int
 
-let head_beta_reduce = ref (fun _ ~upto:_ _ -> assert false);;
+let head_beta_reduce = ref (fun (_:NCicEnvironment.status) ~upto:_ _ -> assert false);;
 let set_head_beta_reduce = (:=) head_beta_reduce;;
 
 let expand_local_context = function
@@ -74,7 +74,7 @@ let map status g k f = function
       | C.Appl l :: tl -> C.Appl (l@tl)
       | l1 -> C.Appl l1
     in
-      if fire_beta then !head_beta_reduce (status :> NCic.status) ~upto t
+      if fire_beta then !head_beta_reduce (status :> NCicEnvironment.status) ~upto t
       else t
  | C.Prod (n,s,t) as orig ->
      let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in
diff --git a/matitaB/components/ng_kernel/nCicUtils.mli b/matitaB/components/ng_kernel/nCicUtils.mli
index 6697e31b5..de56c4e1f 100644
--- a/matitaB/components/ng_kernel/nCicUtils.mli
+++ b/matitaB/components/ng_kernel/nCicUtils.mli
@@ -25,9 +25,9 @@ val fold:
   (NCic.hypothesis -> 'k -> 'k) -> 'k ->
   ('k -> 'a -> NCic.term -> 'a) -> 'a -> NCic.term -> 'a
 val map:
- #NCic.status ->
+ #NCicEnvironment.status ->
  (NCic.hypothesis -> 'k -> 'k) -> 'k ->
  ('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term
 
-val set_head_beta_reduce: (NCic.status -> upto:int -> NCic.term -> NCic.term) -> unit
+val set_head_beta_reduce: (NCicEnvironment.status -> upto:int -> NCic.term -> NCic.term) -> unit
 
diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml
index 6cb4029cf..b775bff00 100644
--- a/matitaB/components/ng_library/nCicLibrary.ml
+++ b/matitaB/components/ng_library/nCicLibrary.ml
@@ -88,8 +88,6 @@ type timestamp =
 ;;
 
 let time0 = [],[];;
-let storage = ref [];;
-let local_aliases = ref [];;
 
 let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
  let global_aliases = ref [] in
@@ -148,23 +146,52 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 
 let init = load_db;;
 
+type db = {
+  storage : 
+    [ `Obj of NUri.uri * NCic.obj 
+    | `Constr of NCic.universe * NCic.universe] list ref;
+  local_aliases : 
+    (NUri.uri * string * NReference.reference) list ref
+}
+
+class type g_status =
+  object
+    method lib_db : db
+  end
+
 class virtual status uid =
  object
-  inherit NCic.status uid
+  inherit NCicEnvironment.status uid
+
+  val lib_db = {
+    storage = ref [];
+    local_aliases = ref []
+  }
+  method lib_db = lib_db
+
   val timestamp = (time0 : timestamp)
   method timestamp = timestamp
+
   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 >}  
  end
 
-let time_travel0 (sto,ali) =
- let diff_len = List.length !storage - List.length sto in
- let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in
+let reset_timestamp st =
+  st#lib_db.storage := [];
+  st#lib_db.local_aliases := []
+;;
+
+let time_travel0 st (sto,ali) =
+ let diff_len = List.length !(st#lib_db.storage) - List.length sto in
+ let to_be_deleted,_ = HExtlib.split_nth diff_len !(st#lib_db.storage) in
   if List.length to_be_deleted > 0 then
-   List.iter NCicEnvironment.invalidate_item to_be_deleted;
-  storage := sto; local_aliases := ali
+   List.iter (NCicEnvironment.invalidate_item st) to_be_deleted;
+  st#lib_db.storage := sto; st#lib_db.local_aliases := ali
 ;;
 
-let time_travel status = time_travel0 status#timestamp;;
+let time_travel status = time_travel0 status status#timestamp;;
 
 type obj = string * Obj.t
 (* includes are transitively closed; dependencies are only immediate *)
@@ -177,8 +204,11 @@ class type g_dumpable_status =
  end
 
 (* uid = None --> single user mode *)
-class dumpable_status =
+class dumpable_status uid =
  object
+  inherit NCicPp.status uid
+  inherit status uid
+
   val db = { objs = []; includes = []; dependencies = [] }
   method dump = db
   method set_dump v = {< db = v >}
@@ -202,7 +232,7 @@ module type SerializerType =
   type 'a register_type =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
-    refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) ->
+    refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) ->
     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
     alias_only:bool ->
      dumpable_status -> dumpable_status
@@ -216,14 +246,14 @@ module type SerializerType =
  end
 
 module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
-  val set: dumpable_s -> dumpable_status -> dumpable_s val user : dumpable_s ->
-  string option end) =
+  val set: dumpable_s -> dumpable_status -> dumpable_s (*val user : dumpable_s ->
+  string option*) end) =
  struct
   type dumpable_status = D.dumpable_s
   type 'a register_type =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
-    refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) ->
+    refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) ->
     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
     alias_only:bool ->
      dumpable_status -> dumpable_status
@@ -252,7 +282,7 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
    end
 
   let serialize ~baseuri status =
-   let ch = open_out (ng_path_of_baseuri (D.user status) baseuri) in
+   let ch = open_out (ng_path_of_baseuri (D.get status)#user baseuri) in
    Marshal.to_channel ch (magic,((D.get status)#dump.dependencies,(D.get status)#dump.objs)) [];
    close_out ch;
    let deps = String.concat ", " ((D.get status)#dump.dependencies) in 
@@ -260,14 +290,14 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
    List.iter
     (function 
      | `Obj (uri,obj) ->
-         let ch = open_out (ng_path_of_baseuri (D.user status) uri) in
+         let ch = open_out (ng_path_of_baseuri (D.get status)#user uri) in
          Marshal.to_channel ch (magic,obj) [];
          close_out ch
      | `Constr _ -> ()
-    ) !storage;
-   set_global_aliases (!local_aliases @ get_global_aliases ());
+    ) !((D.get status)#lib_db.storage);
+   set_global_aliases (!((D.get status)#lib_db.local_aliases) @ get_global_aliases ());
    List.iter (fun u -> add_deps u [baseuri]) (D.get status)#dump.includes;
-   time_travel0 time0
+   reset_timestamp (D.get status)
 
   let require2 ~baseuri ~alias_only status =
    try
@@ -277,11 +307,11 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
       (s#set_dump
         {s#dump with
         includes = baseuri::List.filter ((<>) baseuri) s#dump.includes}) in
-    let _dependencies,dump = require0 (D.user status) ~baseuri in
+    let _dependencies,dump = require0 (D.get status)#user ~baseuri in
      List.fold_right (!require1 ~alias_only) dump status
    with
     Sys_error _ ->
-     raise (IncludedFileNotCompiled(ng_path_of_baseuri (D.user status) baseuri,NUri.string_of_uri baseuri))
+     raise (IncludedFileNotCompiled(ng_path_of_baseuri (D.get status)#user baseuri,NUri.string_of_uri baseuri))
 
   let dependencies_of user ~baseuri = fst (require0 user ~baseuri)
 
@@ -324,24 +354,24 @@ let fetch_obj user status uri =
   refresh_uri_in_obj status obj
 ;;
 
-let resolve name =
+let resolve st name =
  try
   HExtlib.filter_map
    (fun (_,name',nref) -> if name'=name then Some nref else None)
-   (!local_aliases @ get_global_aliases ())
+   (!(st#lib_db.local_aliases) @ get_global_aliases ())
  with
   Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
 ;;
 
-let aliases_of uri =
+let aliases_of st uri =
   HExtlib.filter_map
    (fun (uri',_,nref) ->
-     if NUri.eq uri' uri then Some nref else None) !local_aliases
+     if NUri.eq uri' uri then Some nref else None) !(st#lib_db.local_aliases)
 ;;
 
 let add_obj status ((u,_,_,_,_) as obj) =
  NCicEnvironment.check_and_add_obj status obj;
- storage := (`Obj (u,obj))::!storage;
+ status#lib_db.storage := (`Obj (u,obj))::!(status#lib_db.storage);
   let _,height,_,_,obj = obj in
   let references =
    match obj with
@@ -370,33 +400,35 @@ let add_obj status ((u,_,_,_,_) as obj) =
               (NReference.Ind (inductive,i,leftno))]
          ) il)
   in
-  local_aliases := references @ !local_aliases;
-  status#set_timestamp (!storage,!local_aliases)
+  status#lib_db.local_aliases := references @ !(status#lib_db.local_aliases);
+  status#set_timestamp (!(status#lib_db.storage),!(status#lib_db.local_aliases))
 ;;
 
 let add_constraint status u1 u2 = 
   if
    List.exists
     (function `Constr (u1',u2') when u1=u1' && u2=u2' -> true | _ -> false)
-    !storage
+    !(status#lib_db.storage)
   then
    (*CSC: raise an exception here! *)
    (prerr_endline "CANNOT ADD A CONSTRAINT TWICE"; assert false);
-  NCicEnvironment.add_lt_constraint u1 u2;
-  storage := (`Constr (u1,u2)) :: !storage;
-  status#set_timestamp (!storage,!local_aliases)
+  NCicEnvironment.add_lt_constraint status u1 u2;
+  status#lib_db.storage := (`Constr (u1,u2)) :: !(status#lib_db.storage);
+  status#set_timestamp (!(status#lib_db.storage),!(status#lib_db.local_aliases))
 ;;
 
 let get_obj status u =
+(*
  try 
   List.assq u 
    (HExtlib.filter_map 
     (function `Obj (u,o) -> Some (u,o) | _ -> None )
-    !storage)
- with Not_found ->
+    !(status#lib_db.storage))
+ with Not_found ->*)
   try fetch_obj (status#user) status u
   with Sys_error _ ->
    raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u)))
 ;;
 
-NCicEnvironment.set_get_obj get_obj;;
+NCicEnvironment.set_get_obj 
+  (get_obj :> NCicEnvironment.status -> NUri.uri -> NCic.obj);;
diff --git a/matitaB/components/ng_library/nCicLibrary.mli b/matitaB/components/ng_library/nCicLibrary.mli
index 89e701fc1..cba90c30c 100644
--- a/matitaB/components/ng_library/nCicLibrary.mli
+++ b/matitaB/components/ng_library/nCicLibrary.mli
@@ -16,22 +16,35 @@ exception IncludedFileNotCompiled of string * string
 
 type timestamp
 
+type db
+
+class type g_status =
+  object
+    method lib_db : db
+  end
+
 class virtual status :
  string option ->
  object ('self)
-  inherit NCic.status
+  inherit NCicEnvironment.status
+  inherit g_status
+  method lib_db: db
   method timestamp: timestamp
   method set_timestamp: timestamp -> 'self
+  method set_lib_db: db -> 'self
+  method set_lib_status: #g_status -> 'self
  end
 
 (* it also checks it and add it to the environment *)
 val add_obj: #status as 'status -> NCic.obj -> 'status
 val add_constraint: 
   #status as 'status -> NCic.universe -> NCic.universe -> 'status
-val aliases_of: NUri.uri -> NReference.reference list
-val resolve: string -> NReference.reference list
+val aliases_of: #status -> NUri.uri -> NReference.reference list
+val resolve: #status -> string -> NReference.reference list
+(*
 (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *)
 val get_obj: #NCic.status -> NUri.uri -> NCic.obj (* changes the current timestamp *)
+*)
 
 val time_travel: #status -> unit
 
@@ -45,9 +58,12 @@ class type g_dumpable_status =
   method dump: dump
  end
 
-class dumpable_status : 
+class dumpable_status :
+ string option -> 
  object ('self)
   inherit g_dumpable_status
+  inherit NCicPp.status
+  inherit status
   method set_dump: dump -> 'self
   method set_dumpable_status: #g_dumpable_status -> 'self
  end
@@ -62,7 +78,7 @@ module type SerializerType =
   type 'a register_type =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
-    refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) ->
+    refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) ->
     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
     alias_only:bool ->
      dumpable_status -> dumpable_status
diff --git a/matitaB/components/ng_paramodulation/nCicParamod.mli b/matitaB/components/ng_paramodulation/nCicParamod.mli
index 36c5a7cab..2856ebac9 100644
--- a/matitaB/components/ng_paramodulation/nCicParamod.mli
+++ b/matitaB/components/ng_paramodulation/nCicParamod.mli
@@ -20,9 +20,9 @@ val nparamod :
 type state 
 val empty_state: state
 val forward_infer_step: state -> NCic.term -> NCic.term -> state
-val index_obj: #NCic.status -> state -> NUri.uri -> state
+val index_obj: #NCicEnvironment.status -> state -> NUri.uri -> state
 val is_equation:
- #NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
+ #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
   NCic.term -> bool
 val paramod : 
   #NCicCoercion.status ->
diff --git a/matitaB/components/ng_paramodulation/nCicProof.mli b/matitaB/components/ng_paramodulation/nCicProof.mli
index 5baa10535..78023c0a6 100644
--- a/matitaB/components/ng_paramodulation/nCicProof.mli
+++ b/matitaB/components/ng_paramodulation/nCicProof.mli
@@ -17,7 +17,7 @@ val set_default_sig: unit -> unit
 val get_sig: eq_sig_type -> NCic.term
 
 val mk_proof:
- #NCic.status ->
+ #NCicEnvironment.status ->
   ?demod:bool
   -> NCic.term Terms.bag 
   -> Terms.M.key 
diff --git a/matitaB/components/ng_refiner/nCicMetaSubst.mli b/matitaB/components/ng_refiner/nCicMetaSubst.mli
index c9530d42d..6894129c8 100644
--- a/matitaB/components/ng_refiner/nCicMetaSubst.mli
+++ b/matitaB/components/ng_refiner/nCicMetaSubst.mli
@@ -35,7 +35,7 @@ val maxmeta: unit -> int
  * in the term (for occur check).
  *)
 val delift : 
-  #NCic.status ->
+  #NCicEnvironment.status ->
   unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
     NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) -> 
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
@@ -47,7 +47,7 @@ val delift :
    additional (i.e. l' does not intersects l) positions whose restriction was
    forced because of type dependencies *)
 val restrict: 
-   #NCic.status ->
+   #NCicEnvironment.status ->
     NCic.metasenv ->
     NCic.substitution ->
     int -> int list ->
@@ -65,7 +65,7 @@ val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term
 
 (* returns the resulting type, the metasenv and the arguments *)
 val saturate:
-   #NCic.status ->
+   #NCicEnvironment.status ->
     ?delta:int -> NCic.metasenv -> NCic.substitution -> 
     NCic.context -> NCic.term -> int ->
        NCic.term * NCic.metasenv * NCic.term list
@@ -76,4 +76,4 @@ val is_out_scope_tag : NCic.meta_attrs -> bool
 val int_of_out_scope_tag : NCic.meta_attrs -> int
 
 val is_flexible:
- #NCic.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool
+ #NCicEnvironment.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool
diff --git a/matitaB/components/ng_refiner/nCicRefineUtil.mli b/matitaB/components/ng_refiner/nCicRefineUtil.mli
index 228342378..f87c927d6 100644
--- a/matitaB/components/ng_refiner/nCicRefineUtil.mli
+++ b/matitaB/components/ng_refiner/nCicRefineUtil.mli
@@ -11,10 +11,10 @@
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
-val alpha_equivalence : #NCic.status -> NCic.term -> NCic.term -> bool 
+val alpha_equivalence : #NCicEnvironment.status -> NCic.term -> NCic.term -> bool 
 
 val replace_lifting :
-  #NCic.status ->
+  #NCicEnvironment.status ->
   equality:((string * NCic.context_entry) list ->
             NCic.term -> NCic.term -> bool) ->
   context:(string * NCic.context_entry) list ->
diff --git a/matitaB/components/ng_refiner/nCicRefiner.ml b/matitaB/components/ng_refiner/nCicRefiner.ml
index 4645e6f6e..8deb72797 100644
--- a/matitaB/components/ng_refiner/nCicRefiner.ml
+++ b/matitaB/components/ng_refiner/nCicRefiner.ml
@@ -189,7 +189,7 @@ let rec typeof (status:#NCicCoercion.status)
         in
         metasenv, subst, t, infty
     | C.Sort s -> 
-         (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
+         (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort status s)
          with 
          | NCicEnvironment.UntypableSort msg -> 
               raise (RefineFailure (lazy (localise t, Lazy.force msg)))
@@ -855,7 +855,7 @@ and force_to_sort status metasenv subst context t orig_t localise ty =
         let ty = NCicReduction.whd status ~subst context ty in
           try_coercions status ~localise metasenv subst context
             t orig_t ty (NCic.Sort (NCic.Type 
-              (match NCicEnvironment.get_universes () with
+              (match NCicEnvironment.get_universes status with
                | x::_ -> x 
                | _ -> assert false))) false 
              (Uncertain (lazy (localise orig_t, 
@@ -1204,7 +1204,7 @@ let typeof_obj
                 NCicReduction.whd status ~subst [] ty_sort
                with
                   (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
-                   if not (NCicEnvironment.universe_leq u1 u2) then
+                   if not (NCicEnvironment.universe_leq status u1 u2) then
                     raise
                      (RefineFailure
                        (lazy(localise te, "The type " ^
diff --git a/matitaB/components/ng_refiner/nCicUnifHint.ml b/matitaB/components/ng_refiner/nCicUnifHint.ml
index 960ead117..d228db7b6 100644
--- a/matitaB/components/ng_refiner/nCicUnifHint.ml
+++ b/matitaB/components/ng_refiner/nCicUnifHint.ml
@@ -53,7 +53,7 @@ class type g_status =
 
 class virtual status (uid : string option) =
  object
-  inherit NCic.status uid
+  inherit NCicEnvironment.status uid
   val db = HDB.empty, EQDB.empty
   method uhint_db = db
   method set_uhint_db v = {< db = v >}
diff --git a/matitaB/components/ng_refiner/nCicUnifHint.mli b/matitaB/components/ng_refiner/nCicUnifHint.mli
index 77600663a..fafc4a6f8 100644
--- a/matitaB/components/ng_refiner/nCicUnifHint.mli
+++ b/matitaB/components/ng_refiner/nCicUnifHint.mli
@@ -24,7 +24,7 @@ class virtual status :
  string option ->
  object ('self)
   inherit g_status
-  inherit NCic.status
+  inherit NCicEnvironment.status
   method set_uhint_db: db -> 'self
   method set_unifhint_status: #g_status -> 'self
  end
diff --git a/matitaB/components/ng_refiner/nCicUnification.ml b/matitaB/components/ng_refiner/nCicUnification.ml
index 1e37ff797..cd5c89dd3 100644
--- a/matitaB/components/ng_refiner/nCicUnification.ml
+++ b/matitaB/components/ng_refiner/nCicUnification.ml
@@ -164,7 +164,7 @@ let rec lambda_intros status metasenv subst context argsno ty =
   
 let unopt exc = function None -> raise exc | Some x -> x ;;
 
-let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t =
+let fix (status:#NCicEnvironment.status) metasenv subst is_sup test_eq_only exc t =
   (*D*)  inside 'f'; try let rc =  
   pp (lazy (status#ppterm ~metasenv ~subst ~context:[] t));
   let rec aux test_eq_only metasenv = function
@@ -176,10 +176,10 @@ let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t =
        metasenv,orig
     | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
     | NCic.Sort (NCic.Type u) when is_sup ->
-       metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
+       metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup status u)))
     | NCic.Sort (NCic.Type u) ->
        metasenv, NCic.Sort (NCic.Type 
-         (unopt exc (NCicEnvironment.inf ~strict:false u)))
+         (unopt exc (NCicEnvironment.inf status ~strict:false u)))
     | NCic.Meta (n,_) as orig ->
         (try 
           let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
@@ -335,10 +335,10 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap =
            match s,swap with
               NCic.Type u2, false ->
                NCic.Sort (NCic.Type
-                (unopt exc (NCicEnvironment.inf ~strict:false
-                 (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
+                (unopt exc (NCicEnvironment.inf status ~strict:false
+                 (unopt exc (NCicEnvironment.inf status ~strict:true u1) @ u2))))
             | NCic.Type u2, true ->
-               if NCicEnvironment.universe_lt u2 u1 then
+               if NCicEnvironment.universe_lt status u2 u1 then
                 NCic.Sort (NCic.Type u2)
                else (raise exc)
             | NCic.Prop,_ -> NCic.Sort NCic.Prop
@@ -425,7 +425,7 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
            assert false 
        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
            let a, b = if swap then b,a else a,b in
-           if NCicEnvironment.universe_leq a b then metasenv, subst
+           if NCicEnvironment.universe_leq status a b then metasenv, subst
            else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
        | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
            if NCicEnvironment.universe_eq a b then metasenv, subst
@@ -566,7 +566,7 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
           let tym = NCicSubstitution.subst_meta status lc tym in
            match tyn,tym with
               NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
-               NCicEnvironment.universe_lt u1 u2
+               NCicEnvironment.universe_lt status u1 u2
             | _,_ -> false ->
           instantiate status test_eq_only metasenv subst context m lc'
             (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
diff --git a/matitaB/components/ng_refiner/nCicUnification.mli b/matitaB/components/ng_refiner/nCicUnification.mli
index ec21d6643..d0a539c6a 100644
--- a/matitaB/components/ng_refiner/nCicUnification.mli
+++ b/matitaB/components/ng_refiner/nCicUnification.mli
@@ -25,7 +25,7 @@ val unify :
 
 (* this should be moved elsewhere *)
 val fix_sorts: 
-  #NCic.status -> NCic.metasenv -> NCic.substitution -> 
+  #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> 
     NCic.term -> NCic.metasenv * NCic.term
 
 (* delift_type_wrt_terms st m s c t args
@@ -39,7 +39,7 @@ val delift_type_wrt_terms:
    NCic.metasenv * NCic.substitution * NCic.term
 
 val sortfy :#
- NCic.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context ->
+ NCicEnvironment.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context ->
   NCic.term -> NCic.metasenv * NCic.substitution * NCic.term
 
 val debug : bool ref
diff --git a/matitaB/components/ng_tactics/nCicElim.ml b/matitaB/components/ng_tactics/nCicElim.ml
index c2543711a..fd20de1dc 100644
--- a/matitaB/components/ng_tactics/nCicElim.ml
+++ b/matitaB/components/ng_tactics/nCicElim.ml
@@ -197,7 +197,7 @@ let mk_elims status (uri,_,_,_,obj) =
     NCic.Inductive (true,leftno,[itl],_) ->
       List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s))
        (NCic.Prop::
-         List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+         List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes status))
    | _ -> []
 ;;
 
diff --git a/matitaB/components/ng_tactics/nCicElim.mli b/matitaB/components/ng_tactics/nCicElim.mli
index 826374fab..0d547347d 100644
--- a/matitaB/components/ng_tactics/nCicElim.mli
+++ b/matitaB/components/ng_tactics/nCicElim.mli
@@ -11,8 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val mk_elims: #NCic.status -> NCic.obj -> NotationPt.term NotationPt.obj list
+val mk_elims: #NCicEnvironment.status -> NCic.obj -> NotationPt.term NotationPt.obj list
 val mk_projections:
- #NCic.status -> NCic.obj -> NotationPt.term NotationPt.obj list
+ #NCicEnvironment.status -> NCic.obj -> NotationPt.term NotationPt.obj list
 val ast_of_sort : 
   NCic.sort -> [> `NCProp of string | `NType of string | `Prop ]  * string
diff --git a/matitaB/components/ng_tactics/nCicTacReduction.mli b/matitaB/components/ng_tactics/nCicTacReduction.mli
index b19e57478..c73133f60 100644
--- a/matitaB/components/ng_tactics/nCicTacReduction.mli
+++ b/matitaB/components/ng_tactics/nCicTacReduction.mli
@@ -12,5 +12,5 @@
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
 val normalize:
- #NCic.status -> ?delta:int -> subst:NCic.substitution -> NCic.context ->
+ #NCicEnvironment.status -> ?delta:int -> subst:NCic.substitution -> NCic.context ->
   NCic.term -> NCic.term
diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index 9ef663ee1..f3cd17caf 100644
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -450,7 +450,7 @@ let ground_instances status gl =
            debug_print (lazy (status#ppterm ctx [] [] t));
            List.iter 
              (fun (uri,_,_,_,_) as obj -> 
-                NCicEnvironment.invalidate_item (`Obj (uri, obj))) 
+                NCicEnvironment.invalidate_item status (`Obj (uri, obj))) 
              objs;
            ())
       gl