New experimental commit: metavariables representation is changed again,

[helm.git] / helm / ocaml / cic / cicParser3.ml

diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml
index 82ca496924225edcb6fdf30b41b6fa4e83e78588..72882a186513e62dba5aa9f9dc263d7c9240cefa 100644 (file)
--- 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
 ;;