uses CicPp.ppsort

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index 2c04562d81dcea898ccd3aaf27182ee845c3ace3..1b28e44d0b03632ffaec79d66b37f4948d679e58 100644 (file)
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -116,7 +116,7 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
         ((n+1), from, where)
     | `Sort (sort, positions) ->
         let tbl = MetadataTypes.sort_tbl in
-        let sort_str = MetadataPp.pp_sort sort in
+        let sort_str = CicPp.ppsort sort in
         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
         let where =
           (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::

diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml
index 33f10427ffa41e59f0c8d4a9e83eaeffaf8a5698..e2e21662b371a3c58711d30d569aa4b27ecdc92e 100644 (file)
--- a/helm/ocaml/metadata/metadataPp.ml
+++ b/helm/ocaml/metadata/metadataPp.ml
@@ -57,16 +57,10 @@ let metadata_ns = "http://www.cs.unibo.it/helm/schemas/schema-helm"
 let uri_of_pos pos = String.concat "#" [metadata_ns; pp_position pos]
 *)
 
-let pp_sort = function
-  | Cic.Prop -> "Prop"
-  | Cic.Set -> "Set"
-  | Cic.Type _ -> "Type"
-  | Cic.CProp -> "CProp"
-
 type t = [ `Int of int | `String of string | `Null ]
 
 let columns_of_metadata ~about metadatas =
-  let sort s = `String (pp_sort s) in
+  let sort s = `String (CicPp.ppsort s) in
   let source = `String about in
   let occurrence u = `String u in
   List.fold_left

diff --git a/helm/ocaml/metadata/metadataPp.mli b/helm/ocaml/metadata/metadataPp.mli
index 4ab5f7e76def2821a002d640d34f4b0361cf5ed8..bd37a99595e6fc1c3182df322fb3cde220828158 100644 (file)
--- a/helm/ocaml/metadata/metadataPp.mli
+++ b/helm/ocaml/metadata/metadataPp.mli
@@ -28,7 +28,6 @@
 val pp_position: MetadataTypes.position -> string
 val pp_position_tag: MetadataTypes.position -> string
 (* val pp_constr: MetadataTypes.constr -> string *)
-val pp_sort: Cic.sort -> string
 
 (** Pretty printer and OCamlDBI friendly interface *)