- Some (n,Cic.Def (t,_)) ->
- let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
- Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
- (Some hid);
- (binding::context),
- ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
+ Some (n,Cic.Def (t,ty)) ->
+ let acic =
+ acic_of_cic_context ~computeinnertypes context idrefs t
+ None in
+ let acic2 =
+ acic_of_cic_context ~computeinnertypes context idrefs ty
+ None
+ in
+ Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
+ (Some hid);
+ Hashtbl.replace ids_to_father_ids
+ (CicUtil.id_of_annterm acic2) (Some hid);
+ (binding::context),
+ ((hid,Some (n,Cic.ADef (acic,acic2)))::acontext),
+ (hid::idrefs)