X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=15177ddb1331d04b118eea1838e8a9dd2cbc9c45;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=da4f271b5ae6be34936d6c14cd02b4b6a21a80ab;hpb=f3581a88f462038ba4d97d1702ae86650e269fc5;p=helm.git

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index da4f271b5..15177ddb1 100644
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -71,10 +71,11 @@ let mk_positions positions cur_tbl =
         | `MainConclusion None
         | `MainHypothesis None ->
             sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
-        | `MainConclusion (Some d)
-        | `MainHypothesis (Some d) ->
-            sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
-              cur_tbl pos_str cur_tbl d)
+        | `MainConclusion (Some r)
+        | `MainHypothesis (Some r) ->
+            let depth = MetadataPp.pp_relation r in
+            sprintf "(%s.h_position = \"%s\" and %s.h_depth %s)"
+              cur_tbl pos_str cur_tbl depth)
       (positions :> MetadataTypes.position list)) ^
   ")"
 
@@ -151,7 +152,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
       ((n+2), from, where)
 
 let exec ~(dbd:Mysql.dbd) ?rating (n,from,where) =
-let from = String.concat ", " from in
+  let from = String.concat ", " from in
   let where = String.concat " and " where in
   let query =
     match rating with
@@ -162,7 +163,7 @@ let from = String.concat ", " from in
             and table0.source = hits.source order by hits.no desc")
           from where 
   in
-  prerr_endline query; 
+(*  prerr_endline query; *)
   let result = Mysql.exec dbd query in
   Mysql.map result
     (fun row -> match row.(0) with Some s -> s | _ -> assert false)