else
hd, names, v
in
- let p = C.LetIn (n, v, assert false, p) in
- let it = C.LetIn (n, v, assert false, it) in
- let et = C.LetIn (n, v, assert false, et) in
+ let p = C.LetIn (n, v, x, p) in
+ let it = C.LetIn (n, v, x, it) in
+ let et = C.LetIn (n, v, x, et) in
aux (hd :: c) names p it et tl
| Some (C.Anonymous as n, C.Decl v) as hd :: tl ->
let p = C.Lambda (n, meta, p) in
let et = C.Lambda (n, meta, et) in
aux (hd :: c) names p it et tl
| Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
- let p = C.LetIn (n, meta, assert false, p) in
- let it = C.LetIn (n, meta, assert false, it) in
- let et = C.LetIn (n, meta, assert false, et) in
+ let p = C.LetIn (n, meta, meta, p) in
+ let it = C.LetIn (n, meta, meta, it) in
+ let et = C.LetIn (n, meta, meta, et) in
aux (hd :: c) names p it et tl
| None :: tl -> assert false
in