C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
| C.Meta _ -> t
| C.Sort _ -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| 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)
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
| C.Prod (n,s,t) ->
C.Prod
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| 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.Meta _ as t -> if l = [] then t else C.Appl (t::l)
| C.Sort _ as t -> t (* l should be empty *)
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) ->
C.Cast (reduceaux context l te, reduceaux context l ty)
| C.Prod (name,s,t) ->
eat_first (r,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
- | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let outtype' = reduceaux context [] outtype in
)
| C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
| C.Sort _ as t -> t (* l should be empty *)
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) ->
C.Cast (reduceaux context l te, reduceaux context l ty)
| C.Prod (name,s,t) ->
eat_first (r,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
- | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let outtype' = reduceaux context [] outtype in