| Cic.CurrentProof (_, _, _, _, _, attributes)
| Cic.InductiveDefinition (_, _, _, attributes) ->
attributes
+
+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 rec mk_rels howmany from =
match howmany with
| 0 -> []