| Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
| Break -> []
| Box (_, pl) -> List.flatten (List.map aux pl)
+ | Group pl -> List.flatten (List.map aux pl)
and aux_magic magic =
match magic with
| Opt p ->
| SYMBOL "\\root"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
return_term loc (Layout (Root (arg, index)))
| "hbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (Layout (Box ((H, false, false), p)))
| "vbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (Layout (Box ((V, false, false), p)))
| "hvbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (Layout (Box ((HV, false, false), p)))
| "hovbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (Layout (Box ((HOV, false, false), p)))
| "break" -> return_term loc (Layout Break)
(* | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
| LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (CicNotationUtil.group p)
]
| "simple" NONA
[ i = IDENT -> return_term loc (Variable (TermVar i))