(fun (name,ty,_) (ctx, fixpoints, tys, idx) ->
let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
let r = NReference.reference_of_ouri buri(NReference.CoFix idx) in
- ctx @ [Fix (r,name,ty)], fixpoints_ty @ fixpoints,ty::tys,idx+1)
+ Fix (r,name,ty) :: ctx, fixpoints_ty @ fixpoints,ty::tys,idx+1)
fl ([], [], [], 0)
in
let bctx = bctx @ ctx in
let r =
NReference.reference_of_ouri buri (NReference.Fix (idx,recno))
in
- ctx @ [Fix (r,name,ty)], fixpoints_ty@fixpoints,ty::tys,idx+1)
+ Fix (r,name,ty) :: ctx, fixpoints_ty@fixpoints,ty::tys,idx+1)
fl ([], [], [], 0)
in
let bctx = bctx @ ctx in
let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
| Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
- | Cic.Sort Cic.Set -> NCic.Sort NCic.Set,[]
| Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
| Cic.Sort (Cic.Type _) -> NCic.Sort (NCic.Type 0),[]
+ | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[]
(* calculate depth in the univ_graph*)
| Cic.Appl l ->
let l, fixpoints =