diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 48 |
1 files changed, 31 insertions, 17 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 450b1af0..99264dbe 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -40,7 +40,8 @@ type scope_name = string type goal_reference = | OpenSubgoals | NthGoal of int - | GoalId of goal_identifier + | GoalId of Id.t + | GoalUid of goal_identifier type printable = | PrintTables @@ -155,11 +156,15 @@ type option_value = Goptions.option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option type option_ref_value = | StringRefValue of string | QualidRefValue of reference +(** Identifier and optional list of bound universes. *) +type plident = lident * lident list option + type sort_expr = glob_sort type definition_expr = @@ -168,10 +173,10 @@ type definition_expr = * constr_expr option type fixpoint_expr = - Id.t located * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option + plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option type cofixpoint_expr = - Id.t located * local_binder list * constr_expr * constr_expr option + plident * local_binder list * constr_expr * constr_expr option type local_decl_expr = | AssumExpr of lname * constr_expr @@ -190,11 +195,14 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list type inductive_expr = - lident with_coercion * local_binder list * constr_expr option * inductive_kind * + plident with_coercion * local_binder list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type one_inductive_expr = - lident * local_binder list * constr_expr option * constructor_expr list + plident * local_binder list * constr_expr option * constructor_expr list + +type proof_expr = + plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) type grammar_tactic_prod_item_expr = | TacTerm of string @@ -218,14 +226,21 @@ type scheme = | EqualityScheme of reference or_by_notation type section_subset_expr = - | SsSet of lident list + | SsEmpty + | SsSingl of lident | SsCompl of section_subset_expr | SsUnion of section_subset_expr * section_subset_expr | SsSubstr of section_subset_expr * section_subset_expr + | SsFwdClose of section_subset_expr -type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr - -type extend_name = string * int +(** Extension identifiers for the VERNAC EXTEND mechanism. *) +type extend_name = + (** Name of the vernac entry where the tactic is defined, typically found + after the VERNAC EXTEND statement in the source. *) + string * + (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch + is given an offset, starting from zero. *) + int (* This type allows registering the inlining of constants in native compiler. It will be extended with primitive inductive types and operators *) @@ -273,6 +288,7 @@ type vernac_expr = (* Control *) | VernacLoad of verbose_flag * string | VernacTime of vernac_list + | VernacRedirect of string * vernac_list | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacError of exn (* always fails *) @@ -283,7 +299,7 @@ type vernac_expr = | VernacSyntaxExtension of obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) - | VernacDelimiters of scope_name * string + | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * reference or_by_notation list | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * constr_expr * scope_name option @@ -294,14 +310,12 @@ type vernac_expr = (* Gallina *) | VernacDefinition of - (locality option * definition_object_kind) * lident * definition_expr - | VernacStartTheoremProof of theorem_kind * - (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list * - bool + (locality option * definition_object_kind) * plident * definition_expr + | VernacStartTheoremProof of theorem_kind * proof_expr list * bool | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * - inline * simple_binder with_coercion list + inline * (plident list * constr_expr) with_coercion list | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list @@ -323,7 +337,7 @@ type vernac_expr = class_rawexpr * class_rawexpr | VernacIdentityCoercion of obsolete_locality * lident * class_rawexpr * class_rawexpr - | VernacNameSectionHypSet of lident * section_subset_descr + | VernacNameSectionHypSet of lident * section_subset_expr (* Type classes *) | VernacInstance of @@ -428,7 +442,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * section_subset_descr option + | VernacProof of raw_tactic_expr option * section_subset_expr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn |