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 =
let ty =
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