X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FmetadataQuery.ml;h=cd14f3f5eb8d6be766c272b73e5af3fd9aa730fa;hb=041ad23b567b9844ec187ad436595868441802f4;hp=0dc19582a329261b1d8e43e0b20a0c017b0d6646;hpb=b396fcf2d604ed9b9952217539ff69e2f5fff3c5;p=helm.git

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index 0dc19582a..cd14f3f5e 100644
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -207,6 +207,14 @@ let is_predicate u =
     check_last_pi ty
 ;;
 
+let only constants uri =
+  prerr_endline (UriManager.string_of_uri uri);
+  let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
+  let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+  let consts = Constr.constants_of ty in
+  Constr.UriManagerSet.subset consts constants 
+;;
+
 let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
   let (_, metasenv, _, _) = proof in
   let add_uris_for acc goal =
@@ -245,6 +253,7 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
 *)
   let uris = List.filter nonvar (List.map snd uris) in
   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+  let uris = List.filter (only all_constants_closed) uris in
    uris
 ;;