| 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 ('term,'obj) command =