(** {2 Grammar} *)
-let boxify = function
- | [ a ] -> a
- | l -> Layout (Box (H, l))
-
let fold_binder binder pt_names body =
let fold_cluster binder terms ty body =
List.fold_right
return_term loc (Layout (Box (V, p)))
| SYMBOL "\\BREAK" -> return_term loc (Layout Break)
| DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
- return_term loc (boxify p)
+ return_term loc (CicNotationUtil.boxify p)
| p = SELF; SYMBOL "\\AS"; id = IDENT ->
return_term loc (Variable (Ascription (p, id)))
]