C.ALambda
(fresh_id'',n, aux' context idrefs s,
aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
- | C.LetIn (n,s,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
+ | C.LetIn (n,s,ty,t) ->
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)
+ (fresh_id'', n, aux' context idrefs s, aux' context idrefs ty,
+ aux' ((Some (n, C.Def(s,ty)))::context) (fresh_id''::idrefs) t)
| C.Appl l ->
xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = `Prop then
Hashtbl.add ids_to_hypotheses hid binding ;
incr hypotheses_seed ;
match binding with
- 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)
| Some (n,Cic.Decl t) ->
let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
None -> None
| Some (n, Cic.Decl t)->
Some (n, Cic.Decl (Unshare.unshare t))
- | Some (n, Cic.Def (t,None)) ->
- Some (n, Cic.Def ((Unshare.unshare t),None))
- | Some (n,Cic.Def (bo,Some ty)) ->
- Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
+ | Some (n,Cic.Def (bo,ty)) ->
+ Some (n, Cic.Def (Unshare.unshare bo,Unshare.unshare ty))
in
d::canonical_context'
) canonical_context []
None -> None
| Some (n, C.Decl t)->
Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t))
- | Some (n, C.Def (t,None)) ->
+ | Some (n, C.Def (t,ty)) ->
Some (n,
- C.Def ((eta_fix_and_unshare conjectures canonical_context' t),None))
- | Some (_,C.Def (_,Some _)) -> assert false
+ C.Def
+ (eta_fix_and_unshare conjectures canonical_context' t,
+ eta_fix_and_unshare conjectures canonical_context' ty))
in
d::canonical_context'
) canonical_context []
C.ALambda
(fresh_id,n, aux context s,
aux ((fresh_id, Some (n, C.Decl s))::context) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.ALetIn
- (fresh_id, n, aux context s,
- aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
+ (fresh_id, n, aux context s, aux context ty,
+ aux ((fresh_id, Some (n, C.Def(s,ty)))::context) t)
| C.Appl l ->
C.AAppl (fresh_id, List.map (aux context) l)
| C.Const (uri,exp_named_subst) ->