From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 Oct 2006 14:58:18 +0000 (+0000)
Subject: The type of universe_of_goals has slightly changed, omitting
X-Git-Tag: 0.4.95@7852~868
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1ab2c0adb5418580b7fa3448e62e9495e5fe8362;p=helm.git

The type of universe_of_goals has slightly changed, omitting
to pass a useless proof. A few prerr_endline have been removed.
---

diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml
index 246df0838..9b4f565c8 100644
--- a/components/tactics/metadataQuery.ml
+++ b/components/tactics/metadataQuery.ml
@@ -231,16 +231,16 @@ let only constants 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
-(*  prerr_endline ("XXX " ^ UriManager.string_of_uri uri);*)
-(*  Constr.UriManagerSet.iter (fun u -> prerr_endline (" - " ^*)
-(*  UriManager.string_of_uri u)) consts;*)
-(*  Constr.UriManagerSet.iter (fun u -> prerr_endline (" + " ^*)
-(*  UriManager.string_of_uri u)) constants;*)
+(*
+  prerr_endline ("XXX " ^ UriManager.string_of_uri uri);
+  Constr.UriManagerSet.iter (fun u -> prerr_endline (" - " ^
+ UriManager.string_of_uri u)) consts;
+  Constr.UriManagerSet.iter (fun u -> prerr_endline (" + " ^
+  UriManager.string_of_uri u)) constants;*)
   Constr.UriManagerSet.subset consts constants 
 ;;
 
-let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
-  let (_, metasenv, _, _) = proof in
+let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals =
   let add_uris_for acc goal =
    let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
    let main, sig_constants = Constr.signature_of ty in
@@ -260,7 +260,6 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
   let predicates, rest = 
     Constr.UriManagerSet.partition is_predicate all_constants_closed
   in
-  prerr_endline ("FOO!1");
   let uris =
     Constr.UriManagerSet.fold
       (fun u acc -> 
@@ -271,7 +270,6 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
         acc @ uris)
       predicates []
   in
-  prerr_endline ("FOO!2");
 (*
   let uris =
     sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) 
diff --git a/components/tactics/metadataQuery.mli b/components/tactics/metadataQuery.mli
index 496041554..aebe45198 100644
--- a/components/tactics/metadataQuery.mli
+++ b/components/tactics/metadataQuery.mli
@@ -34,7 +34,7 @@ val signature_of_goal:
     UriManager.uri list
 
 val universe_of_goals:
-  dbd:HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list ->
+  dbd:HMysql.dbd -> Cic.metasenv -> ProofEngineTypes.goal list ->
     UriManager.uri list
 
 val equations_for_goal: