X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=3bc3c566e778ba9a591bc3042c7f3f5a8abbcd4c;hb=927b0dc91ca0369dd029c43ffe9258e17908fa38;hp=b6b360a813a9a3460cda2b39220fae443ac02842;hpb=ecd70e5517095820fad8e4fde6f6424617ac5d44;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index b6b360a81..3bc3c566e 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -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)
@@ -304,5 +304,5 @@ let elim ~dbd uri =
      `Obj (uri,[`InHypothesis]);
     ]
   in
-  MetadataConstraints.at_least ~dbd constraints
+  MetadataConstraints.at_least ~rating:`Hits ~dbd constraints