X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataPp.ml;fp=helm%2Focaml%2Fmetadata%2FmetadataPp.ml;h=63a1a0955a55b8ee1f5189aaa3b58f3672c1e06d;hb=f3581a88f462038ba4d97d1702ae86650e269fc5;hp=5fc05b91dc59fcdc66d24882068b2dad0019f58c;hpb=0ef18c2aaa95d86b3bcdac35d4a14cd4a0cf0fdd;p=helm.git

diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml
index 5fc05b91d..63a1a0955 100644
--- a/helm/ocaml/metadata/metadataPp.ml
+++ b/helm/ocaml/metadata/metadataPp.ml
@@ -85,6 +85,15 @@ let columns_of_metadata metadata =
       (List.append sort_cols s, List.append rel_cols r, List.append obj_cols o))
     ([], [], []) metadata
 
+let pp_constr =
+  function
+    | `Sort (sort, p) -> 
+	sprintf "Sort %s; [%s]" 
+	  (CicPp.ppsort sort) (String.concat ";" (List.map pp_position p))
+    | `Rel p -> sprintf "Rel [%s]" (String.concat ";" (List.map pp_position p))
+    | `Obj (uri, p) -> sprintf "Obj %s; [%s]" 
+	uri (String.concat ";" (List.map pp_position p))
+ 
 (*
 let pp_columns ?(sep = "\n") (sort_cols, rel_cols, obj_cols) =
   String.concat sep