let terms = subst pos env p in
instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
in
- [hovbox false false (instantiate_list [] values)]
+ if values = [] then []
+ else [hovbox false false (instantiate_list [] values)]
| Ast.Opt p ->
let opt_decls = CicNotationEnv.declarations_of_term p in
let env =