- let s' = dummies_of_coercions s in
- let t' = dummies_of_coercions t in
- Cic.Prod (n,s',t')
- | Cic.LetIn(n,s,t) ->
- let s' = dummies_of_coercions s in
- let t' = dummies_of_coercions t in
- Cic.LetIn (n,s',t')
- | Cic.MutCase _ -> prerr_endline "mutcase";Cic.Meta (-1,[])
+ let s' = dummies_of_coercions s in
+ let t' = dummies_of_coercions t in
+ Cic.Prod (n,s',t')
+ | Cic.LetIn(n,s,ty,t) ->
+ let s' = dummies_of_coercions s in
+ let ty' = dummies_of_coercions ty in
+ let t' = dummies_of_coercions t in
+ Cic.LetIn (n,s',ty',t')
+ | Cic.MutCase _ -> Cic.Meta (-1,[])