]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataConstraints.ml
fixed instance
[helm.git] / helm / ocaml / metadata / metadataConstraints.ml
index da4f271b5ae6be34936d6c14cd02b4b6a21a80ab..fe972b0bbd471a667777aff9d8c158998fcf385d 100644 (file)
@@ -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)) ^
   ")"