+let generate_elimination_principles ~add_obj ~add_coercion uri obj =
+ match obj with
+ | Cic.InductiveDefinition (indTypes,_,_,attrs) ->
+ let _,inductive,_,_ = List.hd indTypes in
+ if not inductive then []
+ else
+ let _,all_eliminators =
+ List.fold_left
+ (fun (i,res) _ ->
+ let elim sort =
+ try Some (elim_of ~sort uri i)
+ with Can_t_eliminate -> None
+ in
+ i+1,
+ HExtlib.filter_map
+ elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ] @ res
+ ) (0,[]) indTypes
+ in
+ List.fold_left
+ (fun lemmas (uri,obj) -> add_obj uri obj @ uri::lemmas)
+ [] all_eliminators
+ | _ -> []
+;;
+
+
+let init () =
+ LibrarySync.add_object_declaration_hook generate_elimination_principles;;