- let _,lets =
- List.fold_left
- (fun (context,res) (id,cic) ->
- let ty,_ =
- CicTypeChecker.type_of_aux' [] context cic CicUniv.oblivion_ugraph
- in
- Some (Cic.Name ("H" ^ string_of_int id),
- Cic.Def (cic,ty))::context,res@[id,cic,ty]
- ) (context,[]) lets
+ let lets =
+ List.map (fun (id,cic) -> id,cic,Cic.Implicit (Some `Type)) lets