C.Var (uri,exp_named_subst')
| C.Meta (i,l) ->
let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
- C.Meta (i,l)
+ C.Meta (i,l')
| C.Sort _
| C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
ugraph'
) ugraph cl in
(i + 1),ugraph''
- ) itl (1,ugraph)
+ ) itl (1,ugrap1)
in
ugraph2
| C.Lambda _
| C.LetIn _ ->
raise (AssertFailure (lazy "25"))(* due to type-checking *)
- | C.Appl ((C.MutInd (uri,_,_))::_) as ty
- when uri == coInductiveTypeURI ->
+ | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI ->
guarded_by_constructors ~subst context n nn true te []
coInductiveTypeURI
- | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
+ | C.Appl ((C.MutInd (uri,_,_))::_) ->
guarded_by_constructors ~subst context n nn true te tl
coInductiveTypeURI
| C.Appl _ ->
(lazy (sprintf
("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
(CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
- | C.Appl
- ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
+ | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
if U.eq uri uri' && i = i' then
let params,args =
split tl (List.length tl - k)