differentieted empty substitution list from no substitution given

[helm.git] / helm / ocaml / cic_transformations / ast2pres.ml

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 9679501ab460d2c8ae707edfbc36db396037ac22..dbbfff8e5e0432b2ce9e5064abbdeabf151df217 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -76,7 +76,8 @@ and countterm current_size t =
                let size1 = countvar c var in
                countterm size1 s) current_size l in
          countterm size1 t
-    | A.Ident(s,l) ->
+    | A.Ident(s,None) -> current_size + (String.length s)
+    | A.Ident(s,Some l) ->
         List.fold_left 
          (fun c (v,t) -> countterm (c + (String.length v)) t) 
           (current_size + (String.length s)) l
@@ -218,8 +219,12 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
            | [(s,t)] -> 
                make_subst start_txt s t "]"
            | (s,t)::tl ->
-               (make_subst start_txt s t ";")@(make_substs " " tl) in
-         make_substs "[" subst in
+               (make_subst start_txt s t ";")@(make_substs " " tl)
+          in
+          match subst with
+          | Some subst -> make_substs "[" subst
+          | None -> []
+        in
        Box.V([], (* attr here or on Vbox? *)
              [Box.Text(map_attributes attr,s);
               Box.indent(Box.V([],subst))])