From: Stefano Zacchiroli Date: Fri, 4 Feb 2005 09:14:32 +0000 (+0000) Subject: cosmetic changes X-Git-Tag: V_0_1_0~38 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c4d129e76feb5a393d4fed36a55300f7ef13534;p=helm.git cosmetic changes --- diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index b52f52246..554282589 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -67,7 +67,6 @@ let constr_of_metadata: metadata -> constr = function let sort_tbl_original = "refSort" let rel_tbl_original = "refRel" let obj_tbl_original = "refObj" -let owners_tbl_original = "owners" let conclno_tbl_original = "no_inconcl_aux" let conclno_hyp_tbl_original = "no_concl_hyp" let name_tbl_original = "objectName" @@ -76,7 +75,6 @@ let name_tbl_original = "objectName" let sort_tbl_real = ref sort_tbl_original let rel_tbl_real = ref rel_tbl_original let obj_tbl_real = ref obj_tbl_original -let owners_tbl_real = ref owners_tbl_original let conclno_tbl_real = ref conclno_tbl_original let conclno_hyp_tbl_real = ref conclno_hyp_tbl_original let name_tbl_real = ref name_tbl_original @@ -85,7 +83,6 @@ let name_tbl_real = ref name_tbl_original let sort_tbl () = ! sort_tbl_real ;; let rel_tbl () = ! rel_tbl_real ;; let obj_tbl () = ! obj_tbl_real ;; -let owners_tbl () = ! owners_tbl_real ;; let conclno_tbl () = ! conclno_tbl_real ;; let conclno_hyp_tbl () = ! conclno_hyp_tbl_real ;; let name_tbl () = ! name_tbl_real ;; @@ -95,7 +92,6 @@ let ownerize_tables owner = sort_tbl_real := ( sort_tbl_original ^ "_" ^ owner) ; rel_tbl_real := ( rel_tbl_original ^ "_" ^ owner) ; obj_tbl_real := ( obj_tbl_original ^ "_" ^ owner) ; - owners_tbl_real := ( owners_tbl_original ^ "_" ^ owner) ; conclno_tbl_real := ( conclno_tbl_original ^ "_" ^ owner) ; conclno_hyp_tbl_real := ( conclno_hyp_tbl_original ^ "_" ^ owner) ; name_tbl_real := ( name_tbl_original ^ "_" ^ owner) diff --git a/helm/ocaml/metadata/metadataTypes.mli b/helm/ocaml/metadata/metadataTypes.mli index 2914e97db..86f0df6ec 100644 --- a/helm/ocaml/metadata/metadataTypes.mli +++ b/helm/ocaml/metadata/metadataTypes.mli @@ -57,13 +57,14 @@ type constr = val constr_of_metadata: metadata -> constr + (** invoke this function to set the current owner. Afterwards the functions + * below will return the name of the table of the set owner *) +val ownerize_tables : string -> unit + 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 -