+;;
+
+let generate_projections ~add_obj ~add_coercion (uri as orig_uri) obj =
+ match obj with
+ | Cic.InductiveDefinition (inductivefuns,_,_,attrs) ->
+ let rec get_record_attrs =
+ function
+ | [] -> None
+ | (`Class (`Record fields))::_ -> Some fields
+ | _::tl -> get_record_attrs tl
+ in
+ (match get_record_attrs attrs with
+ | None -> []
+ | Some fields ->
+ let uris = ref [] in
+ let projections =
+ projections_of uri (List.map (fun (x,_,_) -> x) fields)
+ in
+ List.iter2
+ (fun (uri, name, bo) (_name, coercion, arity) ->
+ try
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in
+ let attrs = [`Class `Projection; `Generated] in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ let lemmas = add_obj uri obj in
+ let lemmas1 =
+ if not coercion then [] else
+ add_coercion uri arity 0 (UriManager.buri_of_uri orig_uri)
+ in
+ uris := lemmas1 @ lemmas @ uri::!uris
+ with
+ CicTypeChecker.TypeCheckerFailure s ->
+ HLog.message ("Unable to create projection " ^ name ^
+ " cause: " ^ Lazy.force s);
+ | CicEnvironment.Object_not_found uri ->
+ let depend = UriManager.name_of_uri uri in
+ HLog.message ("Unable to create projection " ^ name ^
+ " because it requires " ^ depend)
+ ) projections fields;
+ !uris)
+ | _ -> []
+;;
+
+
+let init () =
+ LibrarySync.add_object_declaration_hook generate_projections;;