X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser3.ml;h=72882a186513e62dba5aa9f9dc263d7c9240cefa;hb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;hp=82ca496924225edcb6fdf30b41b6fa4e83e78588;hpb=a61f397a3ea3acaf95a04a2aafbf1d3f223a2755;p=helm.git

diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml
index 82ca49692..72882a186 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
 ;;