let metasenv,s = aux metasenv n s in
let metasenv,t = aux metasenv (n+1) t in
metasenv,Cic.Prod(name,s,t)
- | Cic.LetIn(name,s,t) ->
+ | Cic.LetIn(name,s,ty,t) ->
let metasenv,s = aux metasenv n s in
+ let metasenv,ty = aux metasenv n ty in
let metasenv,t = aux metasenv (n+1) t in
- metasenv,Cic.LetIn(name,s,t)
+ metasenv,Cic.LetIn(name,s,ty,t)
| Cic.Const(uri,ens) ->
let metasenv,ens =
List.fold_right