Universes introduction

[helm.git] / helm / ocaml / cic_transformations / cic2Xml.ml

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index d945cc82f63d54b2e931424c625dacd9707ba383..b3467ad9e013ae0b378f7ba081883d6d1c938200 100644 (file)
--- 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
 ;;
@@ -72,9 +72,10 @@ let print_term ~ids_to_inner_sorts =
      | C.ASort (id,s) ->
         let string_of_sort =
          function
-            C.Prop -> "Prop"
-          | C.Set  -> "Set"
-          | C.Type -> "Type"
+            C.Prop  -> "Prop"
+          | C.Set   -> "Set"
+          | C.Type _ -> "Type" (* TASSI *)
+         | C.CProp -> "CProp"
         in
          X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
      | C.AImplicit _ -> raise NotImplemented