]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicParser3.ml
Abst removed from the DTD.
[helm.git] / helm / ocaml / cic / cicParser3.ml
index 72882a186513e62dba5aa9f9dc263d7c9240cefa..8f87504acdc9239e5dd36d49947ad7738b3342a6 100644 (file)
@@ -325,19 +325,6 @@ class eltype_sort =
   end
 ;;
 
-class eltype_abst =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let value = uri_of_xml_attr (n#attribute "uri")
-      and id = string_of_xml_attr (n#attribute "id") in
-       Cic.AAbst (id,value)
-  end
-;;
-
 class eltype_const =
   object (self)
 
@@ -495,7 +482,6 @@ let domspec =
       "LETIN",         (new D.element_impl (new eltype_letin)) ;
       "APPLY",         (new D.element_impl (new eltype_apply)) ;
       "CONST",         (new D.element_impl (new eltype_const)) ;
-      "ABST",          (new D.element_impl (new eltype_abst)) ;
       "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
       "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
       "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;