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 uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
(fun newsubst (uri,t) ->
let t' = eta_fix' context t in
let ty =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
Cic.Variable (_,_,ty,_) ->
CicSubstitution.subst_vars newsubst ty