From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 19 May 2005 10:06:54 +0000 (+0000)
Subject: commented out some debugging messages
X-Git-Tag: single_binding~35
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=87955f4aa47c0f5f416f24bae4848eccb1cc23d5;p=helm.git

commented out some debugging messages
---

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