| Cic.InductiveDefinition (_,_,_,attrs) ->
uris := !uris @
generate_elimination_principles uri refinement_toolkit;
- (* uris := !uris @ generate_inversion refinement_toolkit uri obj; *)
+ uris := !uris @ generate_inversion refinement_toolkit uri obj;
let rec get_record_attrs =
function
| [] -> None