- Cic.Constant (name, Some eliminator_body, eliminator_type, [])
- | _ -> assert false
+ let obj_attrs = [`Class (`Elim sort); `Generated] in
+ Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs)
+ | _ ->
+ failwith (sprintf "not an inductive definition (%s)"
+ (UriManager.string_of_uri uri))