let is_sober c t =
let rec sober_term c g = function
- | C.Rel _
+ | C.Rel i ->
+ if i <= 0 then fun b -> false else g
| C.Sort _
| C.Implicit _ -> g
| C.Const (_, xnss)
| C.LetIn (_, v, ty, t) ->
sober_term c (sober_term c (sober_term c g t) ty) v
| C.Appl []
- | C.Appl [_] -> fun b -> false
+ | C.Appl [_]
+ | C.Appl (C.Appl _ :: _) -> fun b -> false
| C.Appl ts -> sober_terms c g ts
| C.MutCase (_, _, t, v, ts) ->
sober_terms c (sober_term c (sober_term c g t) v) ts