X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=f1c648e9bdef5bb847bebda860df0b42f1cfd1b2;hb=f15a13bab100064a4da238cede323b8d4568c174;hp=b78d1380a603395b6c6d22a00e086375a28acf94;hpb=6104889dac72e3ff37b13ea997dafc4c0ef45ac3;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index b78d1380a..f1c648e9b 100644
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -42,7 +42,7 @@ type cexpr =
     Symbol of string option * string * subst option * string option
                              (* h:xref, name, subst, definitionURL *)
   | LocalVar of (string option) * string        (* h:xref, name *)
-  | Meta of string option * string            (* h:xref, name *)
+  | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
   | Num of string option * string             (* h:xref, value *)
   | Appl of string option * cexpr list        (* h:xref, args *)
   | Binder of string option * string * decl * cexpr   
@@ -58,6 +58,8 @@ and
   def = string * cexpr               (* name, body *)
 and
   subst = (UriManager.uri * cexpr) list
+and
+  meta_subst = cexpr option list
 ;;
 
 (* NOTATION *)
@@ -275,7 +277,15 @@ let acic2cexpr ids_to_inner_sorts t =
     | C.AVar (id,uri,subst) ->
         Symbol (Some id, UriManager.name_of_uri uri, 
           make_subst subst, Some (UriManager.string_of_uri uri))
-    | C.AMeta (id,n,l) -> Meta (Some id,("?" ^ (string_of_int n)))
+    | C.AMeta (id,n,l) ->
+       let l' =
+        List.rev_map
+         (function
+             None -> None
+           | Some t -> Some (acic2cexpr t)
+         ) l
+       in
+        Meta (Some id,("?" ^ (string_of_int n)),l')
     | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
     | C.AImplicit _ -> raise NotImplemented
     | C.AProd (id,n,s,t) ->