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
| Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,n) -> l,n
+ | Cic.InductiveDefinition (l,_,n,_) -> l,n
) in
let (_,_,_,constructors) = List.nth inductive_types tyno in
let constructor_types =
(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,_) ->
+ Cic.Variable (_,_,ty,_,_) ->
CicSubstitution.subst_vars newsubst ty
| _ -> raise ReferenceToNonVariable
in