| C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, liftaux k s, liftaux k ty, liftaux (k+1) t)
| C.Appl l -> C.Appl (List.map (liftaux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
| C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) -> 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.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) -> 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.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
| C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k + 1) t)
| C.Appl l -> C.Appl (List.map (aux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
aux 0 t
;;
+Deannotate.lift := lift;;