]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicParser3.ml
debian version 0.6.3-2
[helm.git] / helm / ocaml / cic / cicParser3.ml
index 02d22b3216b0bf631f2be796689f627a775534be..8e6d276d5c9ea003bc31a6df3197965b4ce5b080 100644 (file)
@@ -53,7 +53,7 @@ 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 ()) (* TASSI: sure? *)
   | _            -> raise (IllFormedXml 2)
 
 let int_of_xml_attr =
@@ -205,7 +205,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
 ;;