commented out some debugging messages

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index d91bec9743aea312a14afda79f891e1744f7a655..f26dae805be9e085a6a8d6d3d58ae7b4265c92c8 100644 (file)
--- 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