X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres.ml;h=f6a3b490d48e4f1e3a717a27ebb015c28e02be31;hb=fc35fbb35a01c110f221c52661f1193ea5664aa6;hp=40f185dcdbc773ed5d2b03b08d8a97ea6074e05a;hpb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml
index 40f185dcd..f6a3b490d 100644
--- a/helm/ocaml/cic_transformations/cexpr2pres.ml
+++ b/helm/ocaml/cic_transformations/cexpr2pres.ml
@@ -49,7 +49,13 @@ let countterm current_size t =
         let c1 = current_size + (String.length name) in 
         countsubst subst c1
     | CE.LocalVar (_,name) -> current_size + (String.length name)
-    | CE.Meta (_,name) -> current_size + (String.length name)
+    | CE.Meta (_,name,l) ->
+       List.fold_left
+        (fun i t ->
+          match t with
+             None -> i
+           | Some t' -> aux i t'
+        ) (current_size + String.length name) l
     | CE.Num (_,value) -> current_size + (String.length value)
     | CE.Appl (_,l) -> 
         List.fold_left aux current_size l
@@ -134,11 +140,20 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow([],P.Mi (attr,name)::tail)
-    | CE.Meta (xref,name) ->
+    | CE.Meta (xref,name,l) ->
         let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow([],P.Mi (attr,name)::tail)
+        let l' =
+         List.map
+          (function
+              None -> P.Mo [] "_"
+            | Some t -> cexpr2pres t
+          ) l
+        in
+         if tail = [] then
+           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+         else
+           P.Mrow
+            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
     | CE.Num (xref,value) -> 
         let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then
@@ -293,11 +308,20 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow ([],P.Mi (attr,name)::tail)
-    | CE.Meta (xref,name) ->
+    | CE.Meta (xref,name,l) ->
         let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow ([],P.Mi (attr,name)::tail)
+        let l' =
+         List.map
+          (function
+              None -> P.Mo [] "_"
+            | Some t -> cexpr2pres t
+          ) l
+        in
+         if tail = [] then
+           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+         else
+           P.Mrow
+            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
     | CE.Num (xref,value) -> 
         let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then