From 87e64c10c39f0adf135ee3633b04b40c1a248825 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 3 Feb 2005 14:32:22 +0000 Subject: [PATCH] added new ownerize function --- helm/ocaml/metadata/metadataTypes.mli | 69 +++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 helm/ocaml/metadata/metadataTypes.mli diff --git a/helm/ocaml/metadata/metadataTypes.mli b/helm/ocaml/metadata/metadataTypes.mli new file mode 100644 index 000000000..1a346595f --- /dev/null +++ b/helm/ocaml/metadata/metadataTypes.mli @@ -0,0 +1,69 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val inconcl_pos : string +val mainconcl_pos : string +val mainhyp_pos : string +val inhyp_pos : string +val inbody_pos : string + +type main_position = + [ `MainConclusion of int option (* Pi depth *) + | `MainHypothesis of int option (* Pi depth *) + ] + +type position = + [ main_position + | `InConclusion + | `InHypothesis + | `InBody + ] + +type pi_depth = int + +type metadata = + [ `Sort of Cic.sort * main_position + | `Rel of main_position + | `Obj of string * position + ] + +type constr = + [ `Sort of Cic.sort * main_position list + | `Rel of main_position list + | `Obj of string * position list + ] + +val constr_of_metadata: metadata -> constr + +val sort_tbl: unit -> string +val rel_tbl: unit -> string +val obj_tbl: unit -> string +val owners_tbl: unit -> string +val conclno_tbl: unit -> string +val conclno_hyp_tbl: unit -> string +val name_tbl: unit -> string + +val ownerize_tables : string -> unit + -- 2.39.2