(string * CicNotationPt.term) list * string * CicNotationPt.term *
(string * CicNotationPt.term) list
-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 ('term,'obj) command =
| Default of loc * string * UriManager.uri list
| Include of loc * string
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
| Obj of loc * 'obj
- | Notation of loc * 'term * Gramext.g_assoc option * int option * 'term
+ | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option *
+ CicNotationPt.term
(* level 1 pattern, associativity, precedence, level 2 pattern *)
- | Interpretation of loc * (string * argument_pattern list) * cic_appl_pattern
+ | Interpretation of loc *
+ string * (string * CicNotationPt.argument_pattern list) *
+ CicNotationPt.cic_appl_pattern
+ (* description (i.e. id), symbol, arg pattern, appl pattern *)
(* DEBUGGING *)
| Dump of loc (* dump grammar on stdout *)