| 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,[]
List.fold_right
(fun luri (l,objs) ->
match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph luri) with
- Cic.Variable (_,bo,_,_,_) ->
- let t =
- match bo with
- None -> List.assoc luri ens
- | Some t -> CicSubstitution.subst_vars ens t in
+ 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