let metasenv,s = aux metasenv n s in
let metasenv,t = aux metasenv (n+1) t in
metasenv,Cic.LetIn(name,s,t)
+ | Cic.Const(uri,ens) ->
+ let metasenv,ens =
+ List.fold_right
+ (fun (v,a) (metasenv,ens) ->
+ let metasenv,a' = aux metasenv n a in
+ metasenv,(v,a')::ens)
+ ens (metasenv,[])
+ in
+ metasenv,Cic.Const(uri,ens)
| t -> metasenv,t
in
aux metasenv 0 p