let sep =
match sep_opt with
| None -> []
- | Some l -> [ Ast.Literal l ]
+ | Some l -> [ Ast.Literal l; break; space ]
in
let rec instantiate_list acc = function
| [] -> List.rev acc
let terms = subst pos env p in
instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
in
- instantiate_list [] values
+ [hovbox false false (instantiate_list [] values)]
| Ast.Opt p ->
let opt_decls = CicNotationEnv.declarations_of_term p in
let env =