acc@[id,real_cic],n+1,h)
([],0,[]) lets
in
- 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
in
let proof,se =
let rec aux se current_proof = function