- | C.AConst (_, u, _)
- | C.AAppl (_, C.AConst (_, u, _) :: _) -> Some (u, 0, 0)
- | C.AMutInd (_, u, i, _)
- | C.AAppl (_, C.AMutInd (_, u, i, _) :: _) -> Some (u, succ i, 0)
- | C.AMutConstruct (_, u, i, j, _)
- | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: _) -> Some (u, succ i, j)
- | _ -> None
+ | C.AConst (_, u, _) ->
+ Some (u, 0, 0, 0)
+ | C.AAppl (_, C.AConst (_, u, _) :: vs) ->
+ Some (u, 0, 0, List.length vs)
+ | C.AMutInd (_, u, i, _) ->
+ Some (u, succ i, 0, 0)
+ | C.AAppl (_, C.AMutInd (_, u, i, _) :: vs) ->
+ Some (u, succ i, 0, List.length vs)
+ | C.AMutConstruct (_, u, i, j, _) ->
+ Some (u, succ i, j, 0)
+ | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: vs) ->
+ Some (u, succ i, j, List.length vs)
+ | _ ->
+ None