(univgraphuri,xmlunivgraphpath) ::
(* now the optional body, both write and register *)
(match bodyxml,bodyuri with
- None,None -> []
+ None,_ -> []
| Some bodyxml,Some bodyuri->
ensure_path_exists xmlbodypath;
Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
| 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