Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
| Cic.CurrentProof _ -> assert false
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 =
) in
let (_,_,_,constructors) = List.nth inductive_types tyno in
let constructor_types =
- Cic.Variable (_,_,ty,_) ->
+ Cic.Variable (_,_,ty,_,_) ->