From 3a396908a6cbf81b6db5032cf9c25860f17b6966 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) --- components/metadata/metadataTypes.ml | 2 +- components/metadata/metadataTypes.mli | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/components/metadata/metadataTypes.ml b/components/metadata/metadataTypes.ml index e186b377a..fd61d717e 100644 --- a/components/metadata/metadataTypes.ml +++ b/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/components/metadata/metadataTypes.mli b/components/metadata/metadataTypes.mli index f86ff84f5..904d837ad 100644 --- a/components/metadata/metadataTypes.mli +++ b/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