From: Andrea Asperti Date: Mon, 27 Nov 2006 12:32:11 +0000 (+0000) Subject: Variant are not indexed. X-Git-Tag: make_still_working~6637 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6c53050aa1e4642a290b00de75f9e68b6f14a35c;p=helm.git Variant are not indexed. --- diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index 9581dc9d6..10dfef58a 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -27,6 +27,12 @@ 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,_,_,_) -> @@ -79,10 +85,15 @@ let add_obj refinement_toolkit uri obj status = 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},