]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataPp.ml
Some modifications due to instance.
[helm.git] / helm / ocaml / metadata / metadataPp.ml
index 5fc05b91dc59fcdc66d24882068b2dad0019f58c..63a1a0955a55b8ee1f5189aaa3b58f3672c1e06d 100644 (file)
@@ -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