| NCic.Prod (name,s,t) as ty ->
let metasenv1, _, arg,_ =
NCicMetaSubst.mk_meta ~attrs:[`Name name] metasenv context
- (`WithType s) in
+ ~with_type:s `IsTerm
+ in
let t, metasenv1, args, pno =
aux metasenv1 (NCicSubstitution.subst arg t)
in
| NCic.LetIn (name,ty,bo,t) ->
let m,_,i,_=
NCicMetaSubst.mk_meta ~attrs:[`Name name] m context
- (`WithType ty)in
+ ~with_type:ty `IsTerm
+ in
let t = NCicSubstitution.subst i t in
aux () (m, (i,bo)::l) t
| t -> NCicUntrusted.map_term_fold_a (fun _ () -> ()) () aux acc t