This commit patches the environment and the library so that their status is

[helm.git] / matitaB / components / ng_kernel / nCicTypeChecker.ml

diff --git a/matitaB/components/ng_kernel/nCicTypeChecker.ml b/matitaB/components/ng_kernel/nCicTypeChecker.ml
index 0a73358e004ad243f18d3f27f4c1d0ab311309d0..489b89287e609473e954c5b94ea005a510b068f0 100644 (file)
--- 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
      | [] -> []