- xxx_add ids_to_inner_sorts fresh_id'' innersort ;
- if innersort = `Prop then
- add_inner_type fresh_id'' ;
- C.ALetIn
- (fresh_id'', n, aux' context idrefs s,
- aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
+ let s_ty =
+ try
+ (cic_CicHash_find terms_to_types s).D.synthesized
+ with
+ Not_found ->
+ cicReduction_whd context (xxx_type_of_aux' metasenv context s);
+ in
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
+ if innersort = `Prop then
+ add_inner_type fresh_id'' ;
+ C.ALetIn
+ (fresh_id'', n, aux' context idrefs s,
+ aux' ((Some (n, C.Def(s,Some s_ty)))::context) (fresh_id''::idrefs) t)