| `IdRef of string (* ACic pointer *)
| `Href of UriManager.uri list (* hyperlinks for literals *)
| `Level of int * Gramext.g_assoc (* precedence, associativity *)
+ | `XmlAttrs of (string option * string * string) list
+ (* list of XML attributes: namespace, name, value *)
]
type literal =
| Root of term * term (* argument, index *)
| Break
| Box of box_spec * term list
+ | Group of term list
and magic_term =
(* level 1 magics *)
(* level 2 variables *)
| FreshVar of string
-type argument_pattern =
- | IdentArg of int * string (* eta-depth, name *)
-
-type cic_appl_pattern =
- | UriPattern of UriManager.uri
- | VarPattern of string
- | ApplPattern of cic_appl_pattern list
-
-type phrase = (* TODO hackish: replace with TacticAst.statement or similar *)
- | Print of term
- | Notation of term * Gramext.g_assoc option * int option * term
- (* level 1 pattern, associativity, precedence, level 2 pattern *)
- | Interpretation of (string * argument_pattern list) * cic_appl_pattern
- | Render of UriManager.uri
-