open Printf
+let is_a_variant obj =
+ match obj with
+ | Cic.Constant(_,_,_,_,attrs) ->
+ List.exists (fun x -> x = `Flavour `Variant) attrs
+ | _ -> false
+
let uris_for_inductive_type uri obj =
match obj with
| Cic.InductiveDefinition(types,_,_,_) ->
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_for_inductive_type uri obj)@lemmas) in
+ uris_to_index
+ in
{status with
GrafiteTypes.objects = uri::status.GrafiteTypes.objects;
GrafiteTypes.universe = universe},
lemmas
-let add_coercion refinement_toolkit ~add_composites status uri arity =
+let add_coercion refinement_toolkit ~add_composites status uri arity baseuri =
let compounds =
- LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity in
+ LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity baseuri in
{status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
compounds