X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser3.ml;h=8f87504acdc9239e5dd36d49947ad7738b3342a6;hb=ab3dd97dbb47ae09a5e90d6d38d3775be7c7ecae;hp=82ca496924225edcb6fdf30b41b6fa4e83e78588;hpb=ae326f646ef4c01b43d6da04201b427d1e175400;p=helm.git

diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml
index 82ca49692..8f87504ac 100644
--- a/helm/ocaml/cic/cicParser3.ml
+++ b/helm/ocaml/cic/cicParser3.ml
@@ -231,8 +231,19 @@ class eltype_meta =
     method to_cic_term =
      let n = self#node in
       let value = int_of_xml_attr (n#attribute "no")
-      and id = string_of_xml_attr (n#attribute "id") in
-       Cic.AMeta (id,value)
+      and id = string_of_xml_attr (n#attribute "id")
+      in
+       let local_context =
+        let sons = n#sub_nodes in
+         List.map
+          (function substitution ->
+            match substitution#sub_nodes with
+               [] -> None
+             | [he] -> Some he#extension#to_cic_term
+             | _ -> raise (IllFormedXml 20)
+          ) sons
+       in
+        Cic.AMeta (id,value,local_context)
   end
 ;;
 
@@ -314,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)
 
@@ -484,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)) ;