| { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
(loc_begin, loc_end)
-
type term_attribute =
- [ `Loc of location (* source file location *)
- | `IdRef of string (* ACic pointer *)
+ [ `Loc of location (* source file location *)
+ | `IdRef of string (* ACic pointer *)
+ | `Href of UriManager.uri list (* hyperlinks for literals *)
+ | `Level of int * Gramext.g_assoc (* precedence, associativity *)
]
type literal =
and subst = string * term
and case_pattern = string * capture_variable list
-and box_kind = H | V
+and box_kind = H | V | HV | HOV
+and box_spec = box_kind * bool * bool (* kind, spacing, indent *)
and layout_pattern =
| Sub of term * term
|+ column separator, row separator +| *)
| Sqrt of term
| Root of term * term (* argument, index *)
- | Break
- | Box of box_kind * term list
+(* | Break *)
+ | Box of box_spec * term list
and magic_term =
(* level 1 magics *)
| FreshVar of string
type argument_pattern =
- | IdentArg of string
- | EtaArg of string option * argument_pattern (* eta abstraction *)
+ | IdentArg of int * string (* eta-depth, name *)
type cic_appl_pattern =
- | UriPattern of string
- | ArgPattern of argument_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