let is_generated obj = List.exists ((=) `Generated) (attributes_of_obj obj)
-let arity_of_composed_coercion obj =
- let attrs = attributes_of_obj obj in
- try
- let tag=List.find (function `Class (`Coercion _) -> true|_->false) attrs in
- match tag with
- | `Class (`Coercion n) -> n
- | _-> assert false
- with Not_found -> 0
-;;
-
let projections_of_record obj uri =
let attrs = attributes_of_obj obj in
try
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