From 5e4a9151cb9c5b9457655a3b2a55fce1ea46f08b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 17 Feb 2004 17:41:33 +0000 Subject: [PATCH] Porting of applyStylesheets.ml to Helm_registry. --- .../ocaml/cic_transformations/applyStylesheets.ml | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/helm/ocaml/cic_transformations/applyStylesheets.ml b/helm/ocaml/cic_transformations/applyStylesheets.ml index fc0a2989c..c72415bcf 100644 --- a/helm/ocaml/cic_transformations/applyStylesheets.ml +++ b/helm/ocaml/cic_transformations/applyStylesheets.ml @@ -130,19 +130,8 @@ let apply_sequent_stylesheets sequent_doc = (*CSC: the getter should handle the innertypes, not the FS *) -let innertypesfile = - try - Sys.getenv "GTOPLEVEL_INNERTYPESFILE" - with - Not_found -> "/public/innertypes" -;; - -let constanttypefile = - try - Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE" - with - Not_found -> "/public/constanttype" -;; +let innertypesfile = Helm_registry.get "gtoplevel.inner_types_file";; +let constanttypefile = Helm_registry.get "gtoplevel.constant_type_file";; let mml_of_cic_sequent metasenv sequent = let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = -- 2.39.2