| C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
| C.Appl l -> C.Appl (List.map (deliftaux k) l)
| C.Const _ as t -> t
- | C.Abst _ as t -> t
| C.MutInd _ as t -> t
| C.MutConstruct _ as t -> t
| C.MutCase (sp,cookingsno,i,outty,t,pl) ->
fo_unif_l subst metasenv (lr1, lr2)
| (C.Const _, _)
| (_, C.Const _)
- | (C.Abst _, _)
- | (_, C.Abst _)
| (C.MutInd _, _)
| (_, C.MutInd _)
| (C.MutConstruct _, _)
List.fold_left
(function metasenv -> aux metasenv k) metasenv l
| C.Const _
- | C.Abst _
| C.MutInd _
| C.MutConstruct _ -> metasenv
| C.MutCase (_,_,_,outty,t,pl) ->
end
| C.Appl _ -> assert false
| C.Const _
- | C.Abst _
| C.MutInd _
| C.MutConstruct _ as t -> t,metasenv
| C.MutCase (sp,cookingsno,i,outty,t,pl) ->
end
| C.Appl _ -> assert false
| C.Const _ as t -> t
- | C.Abst _ as t -> t
| C.MutInd _ as t -> t
| C.MutConstruct _ as t -> t
| C.MutCase (sp,cookingsno,i,outty,t,pl) ->