auto snapshot

[helm.git] / helm / software / components / tactics / metadataQuery.ml

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index 0dc19582a329261b1d8e43e0b20a0c017b0d6646..cd14f3f5eb8d6be766c272b73e5af3fd9aa730fa 100644 (file)
--- 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
 ;;