in
let bctx, fixpoints_tys, tys, _ =
List.fold_right
- (fun (name,ty,_) (ctx, fixpoints, tys, idx) ->
+ (fun (name,ty,_) (bctx, fixpoints, tys, idx) ->
let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
let r = Ref.reference_of_ouri buri(Ref.CoFix idx) in
- Fix (r,name,ty) :: ctx, fixpoints_ty @ fixpoints,ty::tys,idx+1)
+ Fix (r,name,ty) :: bctx, fixpoints_ty @ fixpoints,ty::tys,idx+1)
fl ([], [], [], 0)
in
let bctx = bctx @ ctx in
| Cic.MutConstruct (curi, tyno, consno, ens) ->
aux_ens curi octx ctx n_fix uri ens
(NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno))))
+ | Cic.Var (curi, ens) ->
+ (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+ Cic.Variable (_,Some bo,_,_,_) ->
+ aux octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
+ | _ -> assert false)
| Cic.MutCase (curi, tyno, outty, t, branches) ->
let r = Ref.reference_of_ouri curi (Ref.Ind tyno) in
let outty, fixpoints_outty = aux octx ctx n_fix uri outty in
branches ([],[])
in
NCic.Match (r,outty,t,branches), fixpoints_outty@fixpoints_t@fixpoints
- | Cic.Implicit _ | Cic.Meta _ | Cic.Var _ -> assert false
+ | Cic.Implicit _ | Cic.Meta _ -> assert false
and aux_ens curi octx ctx n_fix uri ens he =
match ens with
[] -> he,[]
let ens,objs =
List.fold_right
(fun luri (l,objs) ->
- let t = List.assoc luri ens in
- let t,o = aux octx ctx n_fix uri t in
- t::l, o@objs
+ match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph luri) with
+ Cic.Variable (_,Some _,_,_,_) -> l, objs
+ | Cic.Variable (_,None,_,_,_) ->
+ let t = List.assoc luri ens in
+ let t,o = aux octx ctx n_fix uri t in
+ t::l, o@objs
+ | _ -> assert false
) params ([],[])
in
NCic.Appl (he::ens),objs