(fun arity (c,saturations) ->
let ty,_ =
CicTypeChecker.type_of_aux' ~subst metasenv context c
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph in
let _,metasenv,args,lastmeta =
TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
let irl =
| Cic.Appl (he::_) -> CicUtil.uri_of_term he
| _ -> CicUtil.uri_of_term t
in
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
| Cic.Constant (_,_, _, _, attrs),_ ->
List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
| _ -> false
| _ -> 0
in
let uri = CicUtil.uri_of_term c in
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
| Cic.Constant (_, _, ty, _, _) -> count_pi ty
| _ -> assert false
in