From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 17 Feb 2004 17:41:33 +0000 (+0000)
Subject: Porting of applyStylesheets.ml to Helm_registry.
X-Git-Tag: v0_0_4~168
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5e4a9151cb9c5b9457655a3b2a55fce1ea46f08b;p=helm.git

Porting of applyStylesheets.ml to Helm_registry.
---

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 =