summaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/misctypes.mli4
-rw-r--r--intf/tacexpr.mli10
-rw-r--r--intf/vernacexpr.mli48
3 files changed, 41 insertions, 21 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 74e13690..5c11119e 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -44,8 +44,8 @@ type 'id move_location =
(** Sorts *)
type 'a glob_sort_gen = GProp | GSet | GType of 'a
-type sort_info = string list
-type level_info = string option
+type sort_info = string Loc.located list
+type level_info = string Loc.located option
type glob_sort = sort_info glob_sort_gen
type glob_level = level_info glob_sort_gen
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index ff090ca8..eb4e5ae7 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -94,8 +94,13 @@ type ('a,'t) match_rule =
| Pat of 'a match_context_hyps list * 'a match_pattern * 't
| All of 't
+(** Extension indentifiers for the TACTIC EXTEND mechanism. *)
type ml_tactic_name = {
+ (** Name of the plugin where the tactic is defined, typically coming from a
+ DECLARE PLUGIN statement in the source. *)
mltac_plugin : string;
+ (** Name of the tactic entry where the tactic is defined, typically found
+ after the TACTIC EXTEND statement in the source. *)
mltac_tactic : string;
}
@@ -109,6 +114,7 @@ type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
type open_constr_expr = unit * constr_expr
type open_glob_constr = unit * glob_constr_and_expr
+type binding_bound_vars = Id.Set.t
type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
type delayed_open_constr_with_bindings =
@@ -320,7 +326,7 @@ constraint 'a = <
type g_trm = glob_constr_and_expr
type g_utrm = g_trm
-type g_pat = glob_constr_and_expr * constr_pattern
+type g_pat = glob_constr_pattern_and_expr
type g_cst = evaluable_global_reference and_short_name or_var
type g_ref = ltac_constant located or_var
type g_nam = Id.t located
@@ -381,7 +387,7 @@ type raw_tactic_arg =
type t_trm = Term.constr
type t_utrm = Glob_term.closed_glob_constr
-type t_pat = glob_constr_and_expr * constr_pattern
+type t_pat = glob_constr_pattern_and_expr
type t_cst = evaluable_global_reference and_short_name
type t_ref = ltac_constant located
type t_nam = Id.t
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