let get_fix_decl (sname, i, w, v) = sname, w in
let get_cofix_decl (sname, w, v) = sname, w in
let rec bc c = function
- | C.LetIn (name, v, t) ->
+ | C.LetIn (name, v, ty, t) ->
let name = mk_fresh_name c name in
- let entry = Some (name, C.Def (v, None)) in
- let v, t = bc c v, bc (entry :: c) t in
- C.LetIn (name, v, t)
+ let entry = Some (name, C.Def (v, ty)) in
+ let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+ C.LetIn (name, v, ty, t)
| C.Lambda (name, w, t) ->
let name = mk_fresh_name c name in
let entry = Some (name, C.Decl w) in
let get_fix_decl (id, sname, i, w, v) = sname, cic w in
let get_cofix_decl (id, sname, w, v) = sname, cic w in
let rec bc c = function
- | C.ALetIn (id, name, v, t) ->
+ | C.ALetIn (id, name, v, ty, t) ->
let name = mk_fresh_name c name in
- let entry = Some (name, C.Def (cic v, None)) in
- let v, t = bc c v, bc (entry :: c) t in
- C.ALetIn (id, name, v, t)
+ let entry = Some (name, C.Def (cic v, cic ty)) in
+ let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+ C.ALetIn (id, name, v, ty, t)
| C.ALambda (id, name, w, t) ->
let name = mk_fresh_name c name in
let entry = Some (name, C.Decl (cic w)) in