| C.MutCase (uri,i,outtype,term,pl) ->
(match term with
C.Rel m when List.mem m safes || m = x ->
| C.MutCase (uri,i,outtype,term,pl) ->
(match term with
C.Rel m when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
- (tys,List.length tl,isinductive,paramsno,cl')
+ (tys@lefts,List.length tl,isinductive,paramsno,cl')
in
let (e,safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
in
let (e,safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
- (tys,List.length tl,isinductive,paramsno,cl')
+ (tys@lefts,List.length tl,isinductive,paramsno,cl')
in
let (e, safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
in
let (e, safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x