let module C = Cic in
function
C.Rel _ as t -> t
- | C.Var _ as t -> t
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst
+ in
+ C.Var (uri,exp_named_subst')
| C.Meta _ as t -> t
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (letin_nf te, letin_nf ty)
| C.Prod (n,s,t) -> C.Prod (n, letin_nf s, letin_nf t)
| C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t)
| C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t
| C.Appl l -> C.Appl (List.map letin_nf 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,outt,t,pl) ->
- C.MutCase (sp,cookingsno,i,letin_nf outt, letin_nf t,
- List.map letin_nf pl)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,typeno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst
+ in
+ C.MutInd (uri,typeno,exp_named_subst')
+ | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst
+ in
+ C.MutConstruct (uri,typeno,consno,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,letin_nf outt, letin_nf t, List.map letin_nf pl)
| C.Fix (i,fl) ->
let substitutedfl =
List.map