| C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
| C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
- | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
| C.Appl (hd :: tl) -> appl_fun um_aux hd tl
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
let t' = apply_subst subst t in
Some (n, Cic.Decl t') :: context
| Some (n, Cic.Def (t, ty)) ->
- let ty' =
- match ty with
- | None -> None
- | Some ty -> Some (apply_subst subst ty)
- in
+ let ty' = apply_subst subst ty in
let t' = apply_subst subst t in
Some (n, Cic.Def (t', ty')) :: context
| None -> None :: context)
(Some n)::name_context
| Some (n,Cic.Def (bo,ty)) ->
sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
- (match ty with
- None -> "_"
- | Some ty -> ppterm_in_name_context ~metasenv subst ty name_context)
+ (ppterm_in_name_context ~metasenv subst ty name_context)
(ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context
| None ->
sprintf "%s_ :? _" (separate i), None::name_context
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
| C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
- | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest)
+ | C.LetIn (name,so,ty,dest) ->
+ C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
| C.Appl l -> C.Appl (List.map (aux k) l)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
force_does_not_occur subst to_be_restricted bo
in
let more_to_be_restricted, ty' =
- match ty with
- | None -> more_to_be_restricted, None
- | Some ty ->
- let more_to_be_restricted', ty' =
- force_does_not_occur subst to_be_restricted ty
- in
- more_to_be_restricted @ more_to_be_restricted',
- Some ty'
+ let more_to_be_restricted', ty' =
+ force_does_not_occur subst to_be_restricted ty
+ in
+ more_to_be_restricted @ more_to_be_restricted',
+ ty'
in
more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
in
| C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
| C.Appl l -> C.Appl (List.map (deliftaux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
let s',subst,metasenv = liftaux subst metasenv k s in
let t',subst,metasenv = liftaux subst metasenv (k+1) t in
C.Lambda (n,s',t'),subst,metasenv
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
let s',subst,metasenv = liftaux subst metasenv k s in
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
let t',subst,metasenv = liftaux subst metasenv (k+1) t in
- C.LetIn (n,s',t'),subst,metasenv
+ C.LetIn (n,s',ty',t'),subst,metasenv
| C.Appl l ->
let l',subst,metasenv =
List.fold_right