let levels_of_term metasenv context term =
let module TC = CicTypeChecker in
let module Red = CicReduction in
let levels_of_term metasenv context term =
let module TC = CicTypeChecker in
let module Red = CicReduction in
degree_aux (Red.whd context u)
in
let entry_eq (s1, b1, v1) (s2, b2, v2) =
degree_aux (Red.whd context u)
in
let entry_eq (s1, b1, v1) (s2, b2, v2) =
- entry_in (Misc.string_of_uriref (uri, tc), main, 2 * v + d - 1) l
+ entry_in (UriManager.string_of_uriref (uri, tc), main, 2 * v + d - 1) l
| Cic.Const (u,exp_named_subst) ->
let l' = inspect_uri main l u [] v term in
inspect_exp_named_subst l' (succ v) exp_named_subst
| Cic.Const (u,exp_named_subst) ->
let l' = inspect_uri main l u [] v term in
inspect_exp_named_subst l' (succ v) exp_named_subst