| Inductive of (string * CicNotationPt.term) list *
CicNotationPt.term inductive_type list
(** parameters, list of loc * mutual inductive types *)
- | Theorem of thm_flavour * string * CicNotationPt.term * CicNotationPt.term option
+ | Theorem of thm_flavour * string * CicNotationPt.term *
+ CicNotationPt.term option
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it
* will be given in proof editing mode using the tactical language
*)
- | Record of
- (string * CicNotationPt.term) list * string * CicNotationPt.term *
+ | Record of (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 *)