| CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
let cic_name = CicNotationUtil.cic_name_of_name name in
| CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
let cic_name = CicNotationUtil.cic_name_of_name name in
- let build_term funs (var,_,_,_) t =
+ let build_term funs (var,_,ty,_) t =
- Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+ Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)