| Symbol_alias of string * int * string (* name, instance no, description *)
| Number_alias of int * string (* instance no, description *)
-type 'term command =
- | Set of loc * string * string
- | Qed of loc
- (** name.
- * Name is needed when theorem was started without providing a name
- *)
- | Inductive of loc * (string * 'term) list * 'term inductive_type list
+type obj =
+ | Inductive of (string * CicAst.term) list * CicAst.term inductive_type list
(** parameters, list of loc * mutual inductive types *)
- | Theorem of loc * thm_flavour * string option * 'term * 'term option
+ | Theorem of thm_flavour * string * CicAst.term * CicAst.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 * CicAst.term) list * string * CicAst.term *
+ (string * CicAst.term) list
+
+type ('term,'obj) command =
+ | Set of loc * string * string
+ | Qed of loc
+ (** name.
+ * Name is needed when theorem was started without providing a name
+ *)
| Coercion of loc * 'term
| Alias of loc * alias_spec
+ (** parameters, name, type, fields *)
+ | Obj of loc * 'obj
type ('term, 'ident) tactical =
| Tactic of loc * ('term, 'ident) tactic
| Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
-type ('term, 'ident) code =
- | Command of loc * 'term command
+type ('term, 'obj, 'ident) code =
+ | Command of loc * ('term,'obj) command
| Macro of loc * 'term macro
(* Macro are substantially queries, but since we are not the kind of
* peolpe that like to push "start" to turn off the computer
* we added this command *)
| Tactical of loc * ('term, 'ident) tactical
-type ('term, 'ident) comment =
+type ('term, 'obj, 'ident) comment =
| Note of loc * string
- | Code of loc * ('term, 'ident) code
+ | Code of loc * ('term, 'obj, 'ident) code
-type ('term, 'ident) statement =
- | Executable of loc * ('term, 'ident) code
- | Comment of loc * ('term, 'ident) comment
+type ('term, 'obj, 'ident) statement =
+ | Executable of loc * ('term, 'obj, 'ident) code
+ | Comment of loc * ('term, 'obj, 'ident) comment