Implemented:

[helm.git] / components / content_pres / termContentPres.ml

diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml
index 4c8bbc7d4e4af42ff8defbee358438dd0f139cf5..96a15c01eb072b874a6facd8d38db242ab677076 100644 (file)
--- a/components/content_pres/termContentPres.ml
+++ b/components/content_pres/termContentPres.ml
@@ -232,12 +232,9 @@ let pp_ast0 t k =
     | Ast.Implicit -> builtin_symbol "?"
     | Ast.Meta (n, l) ->
         let local_context l =
-          CicNotationUtil.dress (builtin_symbol ";")
-            (List.map (function None -> builtin_symbol "_" | Some t -> k t) l)
+            List.map (function None -> None | Some t -> Some (k t)) l
         in
-        hbox false false
-          ([ builtin_symbol "?"; number (string_of_int n) ]
-            @ (if l <> [] then local_context l else []))
+        Ast.Meta(n, local_context l)
     | Ast.Sort sort -> aux_sort sort
     | Ast.Num _
     | Ast.Symbol _