]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/metadataQuery.ml
removed debugging print
[helm.git] / helm / ocaml / tactics / metadataQuery.ml
index b6b360a813a9a3460cda2b39220fae443ac02842..0e86d8ccecf56b8a9005cec598b0e5d585cd875b 100644 (file)
@@ -60,7 +60,7 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
       (fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
 
 let match_term ~(dbd:Mysql.dbd) ty =
-  prerr_endline (CicPp.ppterm ty);
+(*   prerr_endline (CicPp.ppterm ty); *)
   let metadata = MetadataExtractor.compute ~body:None ~ty in
   let constants_no =
     MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)