From 87955f4aa47c0f5f416f24bae4848eccb1cc23d5 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 19 May 2005 10:06:54 +0000 Subject: [PATCH] commented out some debugging messages --- helm/ocaml/tactics/metadataQuery.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index d91bec974..f26dae805 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -194,7 +194,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = let pow = 2 ** (Constr.StringSet.cardinal other_constants) in if ((List.length uris < pow) or (pow <= 0)) then begin - prerr_endline "MetadataQuery: large sig, falling back to old method"; +(* prerr_endline "MetadataQuery: large sig, falling back to old method"; *) filter_uris_forward ~dbd (main, other_constants) uris end else filter_uris_backward ~dbd ~facts (main, other_constants) uris @@ -366,11 +366,11 @@ let fill_with_dummy_constants t = let instance ~dbd t = let t',types = fill_with_dummy_constants t in let metadata = MetadataExtractor.compute ~body:None ~ty:t' in - List.iter +(* List.iter (fun x -> prerr_endline - (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) - metadata; + (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) + metadata; *) let no_concl = MetadataDb.count_distinct `Conclusion metadata in let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in let no_full = MetadataDb.count_distinct `Statement metadata in @@ -390,7 +390,7 @@ let instance ~dbd t = in match (look_for_dummy_main metadata) with | None-> - prerr_endline "Caso None"; +(* prerr_endline "Caso None"; *) (* no dummy in main position *) let metadata = List.filter is_dummy metadata in let constraints = List.map MetadataTypes.constr_of_metadata metadata in @@ -399,8 +399,8 @@ let instance ~dbd t = let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints | Some (depth, dummy_type) -> - prerr_endline - (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); +(* prerr_endline + (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); *) (* a dummy in main position *) let metadata_for_dummy_type = MetadataExtractor.compute ~body:None ~ty:dummy_type in -- 2.39.2