hvbox false true [
aux_var var; space;
builtin_symbol "\\def"; break; top_pos (k s) ];
- break; space; keyword "in" ];
+ break; space; keyword "in"; space ];
break;
k t ])
| Ast.LetRec (rec_kind, funs, where) ->
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 =
(match ty, v with
| Env.ListType ty, Env.ListValue (v :: _) ->
aux ((name, (ty, v)) :: acc) tl
+ | Env.TermType _, Env.TermValue _ ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| _ :: tl -> aux acc tl
(* base pattern may contain only meta names, thus we trash all others *)
(match ty, v with
| Env.ListType ty, Env.ListValue (_ :: vtl) ->
aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
+ | Env.TermType _, Env.TermValue _ ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| binding :: tl -> aux (binding :: acc) tl
| [] -> acc