;;
-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
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))
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^
(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
| [] -> []