X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=b3467ad9e013ae0b378f7ba081883d6d1c938200;hb=275727242ccdce9df01af65f3bfb2d65283fa197;hp=7594ffef1a5c4f57d00ed4631179960b2d44115b;hpb=296b163c8a2b09a6f87cbab15c2016de92fc8e70;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 7594ffef1..b3467ad9e 100644
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2000-2004, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -20,7 +20,7 @@
  * MA  02111-1307, USA.
  * 
  * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
+ * http://helm.cs.unibo.it/
  *)
 
 (*CSC codice cut & paste da cicPp e xmlcommand *)
@@ -30,7 +30,7 @@ exception NotImplemented;;
 
 let dtdname ~ask_dtd_to_the_getter dtd =
  if ask_dtd_to_the_getter then
-  Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+  Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
  else
   "http://mowgli.cs.unibo.it/dtd/" ^ dtd
 ;;
@@ -74,7 +74,7 @@ let print_term ~ids_to_inner_sorts =
          function
             C.Prop  -> "Prop"
           | C.Set   -> "Set"
-          | C.Type  -> "Type"
+          | C.Type _ -> "Type" (* TASSI *)
 	  | C.CProp -> "CProp"
         in
          X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]