From 1ab2c0adb5418580b7fa3448e62e9495e5fe8362 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 20 Oct 2006 14:58:18 +0000 Subject: [PATCH] The type of universe_of_goals has slightly changed, omitting to pass a useless proof. A few prerr_endline have been removed. --- components/tactics/metadataQuery.ml | 16 +++++++--------- components/tactics/metadataQuery.mli | 2 +- 2 files changed, 8 insertions(+), 10 deletions(-) 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: -- 2.39.2