From a0622d3a39cbe6dacc056057ff2527239748b846 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 19 Jul 2006 17:31:20 +0000 Subject: [PATCH] exported position_prefix (so that it can be looked up from elsewhere) --- helm/software/components/metadata/metadataTypes.ml | 2 +- helm/software/components/metadata/metadataTypes.mli | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/components/metadata/metadataTypes.ml b/helm/software/components/metadata/metadataTypes.ml index e186b377a..fd61d717e 100644 --- a/helm/software/components/metadata/metadataTypes.ml +++ b/helm/software/components/metadata/metadataTypes.ml @@ -112,4 +112,4 @@ let library_hits_tbl = hits_tbl_original let are_tables_ownerized () = sort_tbl () <> library_sort_tbl - + diff --git a/helm/software/components/metadata/metadataTypes.mli b/helm/software/components/metadata/metadataTypes.mli index f86ff84f5..904d837ad 100644 --- a/helm/software/components/metadata/metadataTypes.mli +++ b/helm/software/components/metadata/metadataTypes.mli @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +val position_prefix : string + val inconcl_pos : string val mainconcl_pos : string val mainhyp_pos : string -- 2.39.2