| C.Cast (te,ty) -> C.Cast (aux te, aux ty)
| C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux s, aux ty, aux t)
| C.Appl l ->
(* Invariant enforced: no application of an application *)
(match List.map aux l with
find_image_aux (what,with_what)
in
let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
- let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+ let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
let rec substaux k ctx what t =
try
S.lift (k-1) (find_image ctx what t)
| C.Lambda (n,s,t) ->
C.Lambda
(n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.LetIn
- (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
+ (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k ctx what) tl in
C.Prod (n, substaux k s, substaux (k + 1) t)
| C.Lambda (n,s,t) ->
C.Lambda (n, substaux k s, substaux (k + 1) t)
- | C.LetIn (n,s,t) ->
- C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k) tl in
C.Prod (n, subst_term k v, subst_term (succ k) t)
| C.Lambda (n, v, t) ->
C.Lambda (n, subst_term k v, subst_term (succ k) t)
- | C.LetIn (n, v, t) ->
- C.LetIn (n, subst_term k v, subst_term (succ k) t)
+ | C.LetIn (n, v, ty, t) ->
+ C.LetIn (n, subst_term k v, subst_term k ty, subst_term (succ k) t)
| C.Fix (i, fixes) ->
let fixesno = List.length fixes in
let fixes = List.map (subst_fix fixesno k) fixes in
| he::tl -> reduceaux context tl (S.subst he t)
(* when name is Anonimous the substitution should be superfluous *)
)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
reduceaux context l (S.subst (reduceaux context [] s) t)
| C.Appl (he::tl) ->
let tl' = List.map (reduceaux context []) tl in
(* be superfluous *)
aux (he::rev_constant_args) tl (S.subst he t)
end
- | C.LetIn (_,s,t) ->
+ | C.LetIn (_,s,_,t) ->
aux rev_constant_args l (S.subst s t)
| C.Fix (i,fl) ->
let (_,recindex,_,body) = List.nth fl i in
(* when name is Anonimous the substitution should *)
(* be superfluous *)
aux tl (S.subst he t))
- | C.LetIn (_,s,t) -> aux l (S.subst s t)
+ | C.LetIn (_,s,_,t) -> aux l (S.subst s t)
| Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri ->
let recno =
prerr_endline ("cerco : " ^ string_of_int (guess_recno uri)