let levels_of_term metasenv context term =
let module TC = CicTypeChecker in
let module Red = CicReduction in
- let module Misc = MQueryMisc in
let degree t =
let rec degree_aux = function
| Cic.Sort _ -> 1
in
let inspect_uri main l uri tc v term =
let d = degree term in
- 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
in
let rec inspect_term main l v term = match term with
Cic.Rel _ -> l
| Cic.Sort _ -> l
| Cic.Implicit _ -> l
| Cic.Var (u,exp_named_subst) ->
- let l' = inspect_uri main l u [] v term in
+ inspect_exp_named_subst l (succ v) 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