* substitution are not rendered by default, an action is generated

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 65e1c32c7e16ec85a676c4a18e900c03ae54c79f..cafd80c4a855b70a80b226af93bab225b700b10e 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -282,17 +282,28 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
             function
               [] -> []
             | [(s,t)] -> 
-                make_subst start_txt s t "]"
+                make_subst start_txt s t ""
             | (s,t)::tl ->
-                (make_subst start_txt s t ";")@(make_substs " " tl)
+                (make_subst start_txt s t ";")@(make_substs "" tl)
           in
           match subst with
-          | Some subst -> make_substs ((map_tex unicode "subst") ^ "[") subst
-          | None -> []
+          | Some subst ->
+             Box.H([],
+                   [Box.Text(make_std_attributes xref,s);
+                    Box.Action([],
+                      [Box.Text([],"[...]");
+                       Box.H([], [Box.Text([], map_tex unicode "subst" ^ "[");
+                        Box.V([], make_substs "" subst);
+                        Box.Text([], "]")])])])
+          | None -> Box.Text(make_std_attributes xref, s)
         in
-        Box.V([], (* attr here or on Vbox? *)
+        subst
+       (*
+        Box.H([], (* attr here or on Vbox? *)
               [Box.Text(make_std_attributes xref,s);
-               Box.indent(Box.V([],subst))])
+              Box.Action([], [Box.Text([], "[_]"); Box.V([],subst)])])
+               (* Box.indent(Box.V([],subst))]) *)
+       *)
     | A.Implicit -> 
         Box.Text([],"_") (* big? *)
     | A.Meta (n, l) ->
@@ -366,11 +377,11 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
 
   and make_subst start_txt varname body end_txt =
     pretty_append ~tail:[end_txt]
-      [Box.Text([],start_txt);
-       Box.Text([],varname);
-       Box.smallskip;
-       Box.Text([],map_tex unicode "Assign")
-      ]
+      ((if start_txt <> "" then [Box.Text([],start_txt)] else [])@
+       [Box.Text([],varname);
+        Box.smallskip;
+        Box.Text([],map_tex unicode "Assign")
+       ])
       body
             
   and pretty_append ~tail l ast =