let tl' = List.map (eta_fix' context) tl in
let ty,_ =
CicTypeChecker.type_of_aux' metasenv context he
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
fix_according_to_type ty (eta_fix' context he) tl'
(*
let term' = eta_fix' context term in
let patterns' = List.map (eta_fix' context) patterns in
let inductive_types,noparams =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
else
let term_type,_ =
CicTypeChecker.type_of_aux' metasenv context term
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
(match term_type with
C.Appl (hd::params) ->
(fun newsubst (uri,t) ->
let t' = eta_fix' context t in
let ty =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
Cic.Variable (_,_,ty,_,_) ->
CicSubstitution.subst_vars newsubst ty