| 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
let t' = CicUniv.fresh() in
let ugraph1 = CicUniv.add_gt t' t ugraph in
(C.Sort (C.Type t')),ugraph1
let t' = CicUniv.fresh() in
let ugraph1 = CicUniv.add_gt t' t ugraph in
(C.Sort (C.Type t')),ugraph1
| C.Cast (te,ty) as t ->
let _,ugraph1 = type_of_aux ~logger context ty ugraph in
let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
| C.Cast (te,ty) as t ->
let _,ugraph1 = type_of_aux ~logger context ty ugraph in
let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in