let t, _ = aux true oc auxc 0 uri ty in
(name_of s, NCic.Def (t,ty)) :: nc,
Ce (lazy ((name_of s, NCic.Def (t,ty)),[])) :: auxc, e :: oc
let t, _ = aux true oc auxc 0 uri ty in
(name_of s, NCic.Def (t,ty)) :: nc,
Ce (lazy ((name_of s, NCic.Def (t,ty)),[])) :: auxc, e :: oc