X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser3.ml;h=940e03e2b8a8e6e8c3102d81084945cdeca5a595;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=02d22b3216b0bf631f2be796689f627a775534be;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml
index 02d22b321..940e03e2b 100644
--- a/helm/ocaml/cic/cicParser3.ml
+++ b/helm/ocaml/cic/cicParser3.ml
@@ -43,6 +43,11 @@ exception IllFormedXml of int;;
 
 (* Utility functions to map a markup attribute to something useful *)
 
+let uri = ref (UriManager.uri_of_string "cic:/none.con")
+
+let set_uri u = 
+  uri := u
+
 let cic_attr_of_xml_attr =
  function
     Pxp_types.Value s       -> Cic.Name s
@@ -53,7 +58,8 @@ let cic_sort_of_xml_attr =
  function
     Pxp_types.Value "Prop" -> Cic.Prop
   | Pxp_types.Value "Set"  -> Cic.Set
-  | Pxp_types.Value "Type" -> Cic.Type
+  | Pxp_types.Value "Type" -> 
+      Cic.Type (CicUniv.fresh ~uri:!uri ()) (* ORRIBLE HACK *)
   | _            -> raise (IllFormedXml 2)
 
 let int_of_xml_attr =
@@ -205,7 +211,7 @@ class eltype_implicit =
      assert (exp_named_subst = []) ;
      let n = self#node in
       let id = string_of_xml_attr (n#attribute "id") in
-       Cic.AImplicit id
+       Cic.AImplicit (id, None)
   end
 ;;