| 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
+ | 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