+ let add_to_universe (universe,status) uri =
+ let term = CicUtil.term_of_uri uri in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+(* prop filtering
+ let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph in
+ prerr_endline (CicPp.ppterm term);
+ prerr_endline (CicPp.ppterm sort);
+ let tkeys =
+ if sort = Cic.Sort(Cic.Prop) then Universe.keys [] ty
+ else []
+ in
+*)
+ let tkeys = Universe.keys [] ty in
+ let index_cmd =
+ List.map
+ (fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri))
+ tkeys
+ in
+(* prop filtering
+ let universe =
+ if sort = Cic.Sort(Cic.Prop) then
+ Universe.index_term_and_unfolded_term universe [] term ty
+ else universe
+*)
+ let universe = Universe.index_term_and_unfolded_term universe [] term ty
+ in
+ let status = GrafiteTypes.add_moo_content index_cmd status in
+ (universe,status)
+ in
+ let uris_to_index =
+ if is_a_variant obj then []
+ else (uris_for_inductive_type uri obj)@lemmas
+ in
+ let universe,status =
+ List.fold_left add_to_universe
+ (status.GrafiteTypes.universe,status)
+ uris_to_index
+ in
+ {status with
+ GrafiteTypes.objects = uri::status.GrafiteTypes.objects;
+ GrafiteTypes.universe = universe},