in
let branches =
match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
- Cic.InductiveDefinition (il,_,_,_) ->
+ Cic.InductiveDefinition (il,_,leftsno,_) ->
let _,_,_,cl =
try
List.nth il indtype_no
in
let branch,tl = find_and_remove branches in
let (_,_,args),_ = branch in
- if List.length args = count_prod ty then
+ if List.length args = count_prod ty - leftsno then
branch::sort tl cltl
else
raise