From c7d07a062257218e85ae41d2fde6693772550223 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 15 Mar 2005 08:27:10 +0000 Subject: [PATCH] - handle metavariables: if at least one of them is present, then the cardinality constraint is not enforce - commented out debugging prints --- helm/ocaml/tactics/metadataQuery.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 0a1f1ee44..8dcbcd08a 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -64,9 +64,16 @@ let match_term ~(dbd:Mysql.dbd) ty = let constants_no = MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty) in + let full_card = + if CicUtil.is_meta_closed ty then + Some (MetadataConstraints.Eq constants_no) + else + None (* we already require a set of constants to appear, this additional + constraints is useless *) +(* MetadataConstraints.Gt (constants_no - 1) *) + in let constraints = List.map MetadataTypes.constr_of_metadata metadata in - Constr.at_least ~dbd ~full_card:(MetadataConstraints.Eq constants_no) - constraints + Constr.at_least ~dbd ?full_card constraints let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y)) @@ -154,7 +161,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = let hyp_constants = Constr.StringSet.diff (signature_of_hypothesis context) types_constants in -Constr.StringSet.iter prerr_endline hyp_constants; +(* Constr.StringSet.iter prerr_endline hyp_constants; *) let other_constants = Constr.StringSet.union sig_constants hyp_constants in let uris = let pow = 2 ** (Constr.StringSet.cardinal other_constants) in @@ -225,7 +232,7 @@ let experimental_hint let hyp_constants = Constr.StringSet.diff (signature_of_hypothesis context) types_constants in -Constr.StringSet.iter prerr_endline hyp_constants; +(* Constr.StringSet.iter prerr_endline hyp_constants; *) let other_constants = Constr.StringSet.union sig_constants hyp_constants in let uris = let pow = 2 ** (Constr.StringSet.cardinal other_constants) in -- 2.39.2