From 297b0cb44bbe8ec7304ca635c566815167266d4a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Jun 2015 11:28:44 +0200 Subject: Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again. --- intf/vernacexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index b72577e1e0..94e3739d4a 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -292,7 +292,7 @@ type vernac_expr = obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) | VernacDelimiters of scope_name * string option - | VernacBindScope of scope_name * reference or_by_notation list + | VernacBindScope of scope_name * class_rawexpr list | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * constr_expr * scope_name option | VernacNotation of -- cgit v1.2.3 From 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 14 Sep 2015 18:35:48 +0200 Subject: Univs: Add universe binding lists to definitions ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. --- intf/vernacexpr.mli | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index bb0331fcc4..37218fbf91 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -160,6 +160,9 @@ 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 +171,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,14 +193,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 = - lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) + plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) type grammar_tactic_prod_item_expr = | TacTerm of string @@ -305,7 +308,7 @@ type vernac_expr = (* Gallina *) | VernacDefinition of - (locality option * definition_object_kind) * lident * definition_expr + (locality option * definition_object_kind) * plident * definition_expr | VernacStartTheoremProof of theorem_kind * proof_expr list * bool | VernacEndProof of proof_end | VernacExactProof of constr_expr -- cgit v1.2.3 From d37aab528dca587127b9f9944e1521e4fc3d9cc7 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 7 Oct 2015 13:11:52 +0200 Subject: Univs: add Strict Universe Declaration option (on by default) This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option. --- intf/misctypes.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'intf') diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 74e136904d..5c11119ed8 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 -- cgit v1.2.3 From ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Oct 2015 14:11:19 +0200 Subject: Goptions: new value type: optional string These options can be set to a string value, but also unset. Internal data is of type string option. --- intf/vernacexpr.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 37218fbf91..9248fa953c 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -155,6 +155,7 @@ 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 -- cgit v1.2.3 From 9ea8867a0fa8f2a52df102732fdc1a931c659826 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Sep 2015 22:12:25 +0200 Subject: Proof using: let-in policy, optional auto-clear, forward closure* - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using . - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. --- intf/vernacexpr.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 9248fa953c..fd6e1c6ae1 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -225,12 +225,12 @@ 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 - -type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr + | SsFwdClose of section_subset_expr (** Extension identifiers for the VERNAC EXTEND mechanism. *) type extend_name = @@ -336,7 +336,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 @@ -441,7 +441,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 -- cgit v1.2.3 From 33d153a01f2814c6e5486c07257667254b91fa0c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 7 Oct 2015 15:08:27 +0200 Subject: Axioms now support the universe binding syntax. We artificially restrict the syntax though, because it is unclear of what the semantics of several axioms in a row is, in particular about the resolution of remaining evars. --- intf/vernacexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index fd6e1c6ae1..f89f076b5f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -314,7 +314,7 @@ type vernac_expr = | 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 -- cgit v1.2.3 From e9995f6e9f9523d4738d9ee494703b6f96bf995d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Oct 2015 14:36:29 +0200 Subject: Fixing untimely unexpected warning "Collision between bound variables" (#4317). Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables. --- intf/tacexpr.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 2b37c580ea..eb4e5ae7d3 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -114,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 = @@ -325,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 @@ -386,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 -- cgit v1.2.3 From 666568377cbe1c18ce479d32f6359aa61af6d553 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Oct 2015 16:36:53 +0200 Subject: Type delayed_open_constr is now monotonic. --- intf/tacexpr.mli | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 45f482cd44..124d4c0fef 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -122,11 +122,12 @@ 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 = - Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings +type 'a delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } -type delayed_open_constr = - Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr +type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open + +type delayed_open_constr = Term.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr located type intro_patterns = delayed_open_constr intro_pattern_expr located list -- cgit v1.2.3 From fb50a8aaf8826349ac8c3a90a6d9b354b9cf34ca Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 26 Oct 2015 11:50:11 +0100 Subject: Type-safe grammar extensions. --- intf/extend.mli | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) (limited to 'intf') diff --git a/intf/extend.mli b/intf/extend.mli index ad9706f3a5..aa0db52d7f 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -50,3 +50,37 @@ type constr_prod_entry_key = type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen + +(** {5 Type-safe grammar extension} *) + +type ('self, 'a) symbol = +| Atoken : Tok.t -> ('self, Tok.t) symbol +| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist1sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol +| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist0sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol +| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol +| Amodifiers : ('self, 'a) symbol -> ('self, 'a list) symbol +| Aself : ('self, 'self) symbol +| Anext : ('self, 'self) symbol +| Aentry : 'a Entry.t -> ('self, 'a) symbol +| Aentryl : 'a Entry.t * int -> ('self, 'a) symbol + +type ('self, _, 'r) rule = +| Stop : ('self, 'r, 'r) rule +| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule + +type 'a production_rule = +| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule + +type 'a single_extend_statment = + string option * + (** Level *) + gram_assoc option * + (** Associativity *) + 'a production_rule list + (** Symbol list with the interpretation function *) + +type 'a extend_statment = + gram_position option * + 'a single_extend_statment list -- cgit v1.2.3 From 4444f04cfdbe449d184ac1ce0a56eb484805364d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 28 Oct 2015 12:56:29 +0100 Subject: Fixing the return type of the Atoken symbol. --- intf/extend.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/extend.mli b/intf/extend.mli index aa0db52d7f..975f194b07 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -54,7 +54,7 @@ type simple_constr_prod_entry_key = (** {5 Type-safe grammar extension} *) type ('self, 'a) symbol = -| Atoken : Tok.t -> ('self, Tok.t) symbol +| Atoken : Tok.t -> ('self, string) symbol | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol | Alist1sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol -- cgit v1.2.3 From 4e643d134f02cfa9a73754c3cf48048541324834 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 31 Oct 2015 15:49:09 +0100 Subject: Adding syntax "Show id" to show goal named id (shelved or not). --- intf/vernacexpr.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index f89f076b5f..99264dbe0a 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 -- cgit v1.2.3 From cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Dec 2015 15:18:42 +0100 Subject: Dead code from August 2014 in apply in. --- intf/tacexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index eb4e5ae7d3..8c55a57051 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -136,7 +136,7 @@ type 'a gen_atomic_tactic_expr = | TacIntroMove of Id.t option * 'nam move_location | TacExact of 'trm | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * - (clear_flag * 'nam * 'dtrm intro_pattern_expr located option) option + ('nam * 'dtrm intro_pattern_expr located option) option | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option | TacCase of evars_flag * 'trm with_bindings_arg | TacFix of Id.t option * int -- cgit v1.2.3 From 0aba678e885fa53fa649de59eb1d06b4af3a847c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Dec 2015 20:42:07 +0100 Subject: Getting rid of the dynamic node of the tactic AST. --- intf/tacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 73130d3804..ead221c5fb 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -209,7 +209,6 @@ constraint 'a = < (** Possible arguments of a tactic definition *) and 'a gen_tactic_arg = - | TacDynamic of Loc.t * Dyn.t | TacGeneric of 'lev generic_argument | MetaIdArg of Loc.t * bool * string | ConstrMayEval of ('trm,'cst,'pat) may_eval -- cgit v1.2.3 From e181c9b043e64342c1e51763f4fe88c78bc4736d Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 12:20:47 +0100 Subject: CLEANUP: Vernacexpr.vernac_expr Originally, "VernacTime" and "VernacRedirect" were defined like this: type vernac_expr = ... | VernacTime of vernac_list | VernacRedirect of string * vernac_list ... where type vernac_list = located_vernac_expr list Currently, that list always contained one and only one element. So I propose changing the definition of these two variants in the following way: | VernacTime of located_vernac_expr | VernacRedirect of string * located_vernac_expr which covers all our current needs and enforces the invariant related to the number of commands that are part of the "VernacTime" and "VernacRedirect" variants. --- intf/vernacexpr.mli | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 99264dbe0a..32c0f29751 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -287,8 +287,8 @@ type module_binder = bool option * lident list * module_ast_inl type vernac_expr = (* Control *) | VernacLoad of verbose_flag * string - | VernacTime of vernac_list - | VernacRedirect of string * vernac_list + | VernacTime of located_vernac_expr + | VernacRedirect of string * located_vernac_expr | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacError of exn (* always fails *) @@ -386,8 +386,7 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of - (rec_flag * (reference * bool * raw_tactic_expr) list) + | VernacDeclareTacticDefinition of (reference * bool * raw_tactic_expr) list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr @@ -455,8 +454,6 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr -and vernac_list = located_vernac_expr list - and located_vernac_expr = Loc.t * vernac_expr (* A vernac classifier has to tell if a command: -- cgit v1.2.3 From 722d369d1bd5a0f65b401f24d6500d5496b8e8ab Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:14:59 +0100 Subject: COMMENTS: added to some variants of the "Constrexpr.prim_token" type. --- intf/constrexpr.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 79f4e99e1f..6543db6a17 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -32,7 +32,9 @@ type abstraction_kind = AbsLambda | AbsPi type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) -type prim_token = Numeral of Bigint.bigint | String of string +type prim_token = + | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *) + | String of string type raw_cases_pattern_expr = | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t -- cgit v1.2.3 From 7a373e3853256b518d8ccb69fa6282211d500e0c Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:21:38 +0100 Subject: COMMENTS: added to some variants of "Glob_term.glob_constr" type. --- intf/glob_term.mli | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'intf') diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 32cf9eaf13..dfcd4a67d3 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -29,9 +29,14 @@ type cases_pattern = | PatCstr of Loc.t * constructor * cases_pattern list * Name.t (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) +(** Representation of an internalized (or in other words globalized) term. *) type glob_constr = | GRef of (Loc.t * global_reference * glob_level list option) + (** An identifier that represents a reference to an object defined + either in the (global) environment or in the (local) context. *) | GVar of (Loc.t * Id.t) + (** An identifier that cannot be regarded as "GRef". + Bound variables are typically represented this way. *) | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list @@ -39,8 +44,7 @@ type glob_constr = | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GLetIn of Loc.t * Name.t * glob_constr * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses - (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in - [MatchStyle]) *) + (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr -- cgit v1.2.3 From e4423ce78823ad9dd8c726e31de712e67a91893a Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:22:49 +0100 Subject: COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type. --- intf/misctypes.mli | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 5c11119ed8..65c7dccf2a 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -43,7 +43,10 @@ type 'id move_location = (** Sorts *) -type 'a glob_sort_gen = GProp | GSet | GType of 'a +type 'a glob_sort_gen = + | GProp (** representation of [Prop] literal *) + | GSet (** representation of [Set] literal *) + | GType of 'a (** representation of [Type] literal *) type sort_info = string Loc.located list type level_info = string Loc.located option -- cgit v1.2.3 From 493b5d18971c8c19eaeccfc992d1212c6479d227 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:38:19 +0100 Subject: CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular command is mapped. --- intf/vernacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 32c0f29751..0e659459e9 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -420,7 +420,6 @@ type vernac_expr = | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list - | VernacNop (* Stm backdoor *) | VernacStm of vernac_expr stm_vernac -- cgit v1.2.3 From 20641795624dbb03da0401e4dc503660e5e73df6 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:50:40 +0100 Subject: CLEANUP: Vernacexpr.VernacDeclareTacticDefinition The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that. --- intf/vernacexpr.mli | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 0e659459e9..07a206b53e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -386,7 +386,7 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of (reference * bool * raw_tactic_expr) list + | VernacDeclareTacticDefinition of tacdef_body list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr @@ -453,6 +453,10 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr +and tacdef_body = + | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + and located_vernac_expr = Loc.t * vernac_expr (* A vernac classifier has to tell if a command: -- cgit v1.2.3 From 5824a2c9362a6e33eb43b5e0e2c7572abeee2511 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:41:58 +0100 Subject: CLEANUP: removing unnecessary alias --- intf/vernacexpr.mli | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 07a206b53e..4bc3a9e609 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -19,7 +19,6 @@ open Libnames type lident = Id.t located type lname = Name.t located type lstring = string located -type lreference = reference type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation @@ -330,8 +329,8 @@ type vernac_expr = | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of - lreference option * export_flag option * lreference list - | VernacImport of export_flag * lreference list + reference option * export_flag option * reference list + | VernacImport of export_flag * reference list | VernacCanonical of reference or_by_notation | VernacCoercion of obsolete_locality * reference or_by_notation * class_rawexpr * class_rawexpr -- cgit v1.2.3 From 1b5f85d38db7a0d7cb9a4b9491a5563461373182 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 17:31:25 +0100 Subject: CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified --- intf/constrexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 6543db6a17..8eff327dcd 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -93,7 +93,7 @@ type constr_expr = | CDelimiters of Loc.t * string * constr_expr and case_expr = - constr_expr * (Name.t located option * cases_pattern_expr option) + constr_expr * Name.t located option * cases_pattern_expr option and branch_expr = Loc.t * cases_pattern_expr list located list * constr_expr -- cgit v1.2.3 From daa7cb065a238c7d4ee394e00315d66d023e5259 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Dec 2015 17:55:25 +0100 Subject: Removing auto from the tactic AST. --- intf/tacexpr.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index ead221c5fb..aa1088c9ea 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -162,10 +162,6 @@ type 'a gen_atomic_tactic_expr = rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis - (* Automation tactics *) - | TacTrivial of debug * 'trm list * string list option - | TacAuto of debug * int or_var option * 'trm list * string list option - (* Context management *) | TacClear of bool * 'nam list | TacClearBody of 'nam list -- cgit v1.2.3 From 203b0eaac832af3b62e484c1aef89a02ffe8e29b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Dec 2015 18:31:17 +0100 Subject: External tactics and notations now accept any tactic argument. This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant. --- intf/tacexpr.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index aa1088c9ea..6d10ef9d51 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -292,9 +292,9 @@ and 'a gen_tactic_expr = | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located (* For ML extensions *) - | TacML of Loc.t * ml_tactic_entry * 'l generic_argument list + | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list (* For syntax extensions *) - | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list + | TacAlias of Loc.t * KerName.t * (Id.t * 'a gen_tactic_arg) list constraint 'a = < term:'t; -- cgit v1.2.3 From f3e611b2115b425f875e971ac9ff7534c2af2800 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 31 Dec 2015 13:56:40 +0100 Subject: Separation of concern in TacAlias API. The TacAlias node now only contains the arguments fed to the tactic notation. The binding variables are worn by the tactic representation in Tacenv. --- intf/tacexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 6d10ef9d51..05e7ea1a3b 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -294,7 +294,7 @@ and 'a gen_tactic_expr = (* For ML extensions *) | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list (* For syntax extensions *) - | TacAlias of Loc.t * KerName.t * (Id.t * 'a gen_tactic_arg) list + | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list constraint 'a = < term:'t; -- cgit v1.2.3 From a5e1b40b93e47a278746ee6752474891cd856c29 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 31 Dec 2015 19:26:02 +0100 Subject: Simplification of grammar_prod_item type. Actually the identifier was never used and just carried along. --- intf/vernacexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 4bc3a9e609..3bb86fcb20 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -205,7 +205,7 @@ type proof_expr = type grammar_tactic_prod_item_expr = | TacTerm of string - | TacNonTerm of Loc.t * string * (Names.Id.t * string) option + | TacNonTerm of Loc.t * string * (Names.Id.t * string) type syntax_modifier = | SetItemLevel of string list * Extend.production_level -- cgit v1.2.3 From a1aff01d16bad2f44392fd5cb804092e12e558ed Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:19:51 +0100 Subject: CLEANUP: removing unused field I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around. --- intf/constrexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 8eff327dcd..eaaf2dbb9f 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -75,7 +75,7 @@ type constr_expr = | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list - | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list + | CRecord of Loc.t * (reference * constr_expr) list | CCases of Loc.t * case_style * constr_expr option * case_expr list * branch_expr list | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) * -- cgit v1.2.3 From b193c6791c16817047b34f0929b1a9817ec62ee1 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 17:57:30 +0100 Subject: COMMENTS: added to the "Constrexpr.CCases" variant. --- intf/constrexpr.mli | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index eaaf2dbb9f..34dc1c6691 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -76,8 +76,14 @@ type constr_expr = | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list | CRecord of Loc.t * (reference * constr_expr) list - | CCases of Loc.t * case_style * constr_expr option * - case_expr list * branch_expr list + + (* representation of the "let" and "match" constructs *) + | CCases of Loc.t (* position of the "match" keyword *) + * case_style (* determines whether this value represents "let" or "match" construct *) + * constr_expr option (* return-clause *) + * case_expr list + * branch_expr list (* branches *) + | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) * constr_expr * constr_expr | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option) @@ -92,8 +98,9 @@ type constr_expr = | CPrim of Loc.t * prim_token | CDelimiters of Loc.t * string * constr_expr -and case_expr = - constr_expr * Name.t located option * cases_pattern_expr option +and case_expr = constr_expr (* expression that is being matched *) + * Name.t located option (* as-clause *) + * cases_pattern_expr option (* in-clause *) and branch_expr = Loc.t * cases_pattern_expr list located list * constr_expr -- cgit v1.2.3 From 51b2581d027528c8e4a347f157baf51a71b9d613 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:39:57 +0100 Subject: CLEANUP: removing unnecessary wrapper --- intf/vernacexpr.mli | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 3bb86fcb20..f763ba6cf8 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -286,8 +286,8 @@ type module_binder = bool option * lident list * module_ast_inl type vernac_expr = (* Control *) | VernacLoad of verbose_flag * string - | VernacTime of located_vernac_expr - | VernacRedirect of string * located_vernac_expr + | VernacTime of vernac_expr located + | VernacRedirect of string * vernac_expr located | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacError of exn (* always fails *) @@ -456,8 +456,6 @@ and tacdef_body = | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) -and located_vernac_expr = Loc.t * vernac_expr - (* A vernac classifier has to tell if a command: vernac_when: has to be executed now (alters the parser) or later vernac_type: if it is starts, ends, continues a proof or -- cgit v1.2.3 From 8a3b19b62720e2324ef24003407c2e83335a51a5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 16 Jan 2016 14:57:48 +0100 Subject: Separating the parsing of user-defined entries from their intepretation. --- intf/extend.mli | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'intf') diff --git a/intf/extend.mli b/intf/extend.mli index 975f194b07..651fa638b5 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -51,6 +51,18 @@ type constr_prod_entry_key = type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen +(** {5 AST for user-provided entries} *) + +type user_symbol = +| Ulist1 : user_symbol -> user_symbol +| Ulist1sep : user_symbol * string -> user_symbol +| Ulist0 : user_symbol -> user_symbol +| Ulist0sep : user_symbol * string -> user_symbol +| Uopt : user_symbol -> user_symbol +| Umodifiers : user_symbol -> user_symbol +| Uentry : string -> user_symbol +| Uentryl : string * int -> user_symbol + (** {5 Type-safe grammar extension} *) type ('self, 'a) symbol = -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- intf/constrexpr.mli | 2 +- intf/decl_kinds.mli | 2 +- intf/evar_kinds.mli | 2 +- intf/extend.mli | 2 +- intf/genredexpr.mli | 2 +- intf/glob_term.mli | 2 +- intf/locus.mli | 2 +- intf/misctypes.mli | 2 +- intf/notation_term.mli | 2 +- intf/pattern.mli | 2 +- intf/tacexpr.mli | 2 +- intf/vernacexpr.mli | 2 +- 12 files changed, 12 insertions(+), 12 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 79f4e99e1f..dcdbd47f68 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* > quotation to insert foreign code as $foo, but it actually only survived in the implementation of Tauto. With the removal of the quotation feature, this is now totally obsolete. --- intf/tacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 57c61874a5..502f2db4c1 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -206,7 +206,6 @@ constraint 'a = < and 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument - | MetaIdArg of Loc.t * bool * string | ConstrMayEval of ('trm,'cst,'pat) may_eval | UConstr of 'utrm | Reference of 'ref -- cgit v1.2.3 From 4d25b224b91959b85fcd68c825a307ec684f0bac Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 28 Feb 2016 18:28:14 +0100 Subject: Printing notations: Cleaning in anticipation of fixing #4592. - Making a clear distinction between expressions of the notation which are associated to binding variables only (as in `Notation "'lam' x , P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))') and those which are associated to at list one subterm (e.g. `Notation "x .+1" := (S x)' but also "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))' as in #4592). The former have type NtnTypeOnlyBinder. - Thus avoiding in particular encoding too early Anonymous as GHole and "Name id" as "GVar id". There is a non-trivial alpha-conversion work to do to get #4592 working. See comments in Notation_ops.add_env. --- intf/notation_term.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 3a643b99b2..39a36310d1 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -61,7 +61,7 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) type notation_var_instance_type = - | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList + | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList (** Type of variables when interpreting a constr_expr as an notation_constr: in a recursive pattern x..y, both x and y carry the individual type -- cgit v1.2.3 From 48327426b59144f1a7181092068077c5a6df7c60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 10:45:31 +0100 Subject: Moving the "fix" tactic to TACTIC EXTEND. --- intf/tacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 502f2db4c1..3993f1b371 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -145,7 +145,6 @@ type 'a gen_atomic_tactic_expr = ('nam * 'dtrm intro_pattern_expr located option) option | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option | TacCase of evars_flag * 'trm with_bindings_arg - | TacFix of Id.t option * int | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list | TacCofix of Id.t option | TacMutualCofix of Id.t * (Id.t * 'trm) list -- cgit v1.2.3 From bda8b2e8f90235ca875422f211cb781068b20b3c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 10:54:08 +0100 Subject: Moving the "cofix" tactic to TACTIC EXTEND. --- intf/tacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 3993f1b371..33a96150c1 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -146,7 +146,6 @@ type 'a gen_atomic_tactic_expr = | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option | TacCase of evars_flag * 'trm with_bindings_arg | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list - | TacCofix of Id.t option | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of bool * 'tacexpr option * -- cgit v1.2.3 From d0bc16d1a0626f4137797bbf0c91e972a0ff43ac Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:05:26 +0100 Subject: Moving the "clear" tactic to TACTIC EXTEND. --- intf/tacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 33a96150c1..10c616627a 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -161,7 +161,6 @@ type 'a gen_atomic_tactic_expr = | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis (* Context management *) - | TacClear of bool * 'nam list | TacClearBody of 'nam list | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list -- cgit v1.2.3 From 7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:20:26 +0100 Subject: Moving the "clearbody" tactic to TACTIC EXTEND. --- intf/tacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 10c616627a..d936748f2d 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -161,7 +161,6 @@ type 'a gen_atomic_tactic_expr = | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis (* Context management *) - | TacClearBody of 'nam list | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list -- cgit v1.2.3 From 6c4fcb156dea5a71fd227606b87333ae00aacb69 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:35:34 +0100 Subject: Moving the "generalize dependent" tactic to TACTIC EXTEND. --- intf/tacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index d936748f2d..52c07e089a 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -151,7 +151,6 @@ type 'a gen_atomic_tactic_expr = bool * 'tacexpr option * 'dtrm intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list - | TacGeneralizeDep of 'trm | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * intro_pattern_naming_expr located option -- cgit v1.2.3 From ae3bbff3ca2564fe24bdf3dd517c82807eae9151 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 12:11:52 +0100 Subject: Moving the "symmetry" tactic to TACTIC EXTEND. --- intf/tacexpr.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 52c07e089a..3f1d0fd76c 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -170,9 +170,6 @@ type 'a gen_atomic_tactic_expr = | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr | TacChange of 'pat option * 'dtrm * 'nam clause_expr - (* Equivalence relations *) - | TacSymmetry of 'nam clause_expr - (* Equality and inversion *) | TacRewrite of evars_flag * (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * -- cgit v1.2.3 From 293222e49ff81bc1299b3822d2a8c526ca803307 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 12:40:45 +0100 Subject: Moving the "exists" tactic to TACTIC EXTEND. --- intf/tacexpr.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 3f1d0fd76c..dae960e0e5 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -163,9 +163,6 @@ type 'a gen_atomic_tactic_expr = | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list - (* Trmuctors *) - | TacSplit of evars_flag * 'trm bindings list - (* Conversion *) | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr | TacChange of 'pat option * 'dtrm * 'nam clause_expr -- cgit v1.2.3 From 1397f791b1699b0f04d971465270d5b2df9a6d7f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 13:32:39 +0100 Subject: Moving the "move" tactic to TACTIC EXTEND. --- intf/tacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index dae960e0e5..7366bc03e6 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -160,7 +160,6 @@ type 'a gen_atomic_tactic_expr = | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis (* Context management *) - | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list (* Conversion *) -- cgit v1.2.3 From 098d283e58966124cfe0e97a3229a9e7e6284120 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Mar 2016 15:04:35 +0100 Subject: Removing the UConstr entry of the tactic_arg AST. This was redundant with the wit_uconstr generic argument, so there was no real point on keeping it there. --- intf/tacexpr.mli | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 7366bc03e6..f2a567c00d 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -180,7 +180,6 @@ type 'a gen_atomic_tactic_expr = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -195,7 +194,6 @@ constraint 'a = < and 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval - | UConstr of 'utrm | Reference of 'ref | TacCall of Loc.t * 'ref * 'a gen_tactic_arg list @@ -206,7 +204,6 @@ and 'a gen_tactic_arg = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -285,7 +282,6 @@ and 'a gen_tactic_expr = constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -300,7 +296,6 @@ and 'a gen_tactic_fun_ast = constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -313,7 +308,6 @@ constraint 'a = < (** Globalized tactics *) type g_trm = glob_constr_and_expr -type g_utrm = g_trm 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 @@ -321,7 +315,6 @@ type g_nam = Id.t located type g_dispatch = < term:g_trm; - utrm:g_utrm; dterm:g_trm; pattern:g_pat; constant:g_cst; @@ -343,7 +336,6 @@ type glob_tactic_arg = (** Raw tactics *) type r_trm = constr_expr -type r_utrm = r_trm type r_pat = constr_pattern_expr type r_cst = reference or_by_notation type r_ref = reference @@ -352,7 +344,6 @@ type r_lev = rlevel type r_dispatch = < term:r_trm; - utrm:r_utrm; dterm:r_trm; pattern:r_pat; constant:r_cst; @@ -374,7 +365,6 @@ type raw_tactic_arg = (** Interpreted tactics *) type t_trm = Term.constr -type t_utrm = Glob_term.closed_glob_constr type t_pat = constr_pattern type t_cst = evaluable_global_reference type t_ref = ltac_constant located @@ -382,7 +372,6 @@ type t_nam = Id.t type t_dispatch = < term:t_trm; - utrm:t_utrm; dterm:g_trm; pattern:t_pat; constant:t_cst; -- cgit v1.2.3 From 6ecbc9990a49a0dd51970c7fc8b13f39f02be773 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 18:34:39 +0100 Subject: Moving Ltac traces to Tacexpr and Tacinterp. --- intf/tacexpr.mli | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index f2a567c00d..b1dc174d4b 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -394,3 +394,15 @@ type tactic_arg = type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen + +(** Traces *) + +type ltac_call_kind = + | LtacMLCall of glob_tactic_expr + | LtacNotationCall of KerName.t + | LtacNameCall of ltac_constant + | LtacAtomCall of glob_atomic_tactic_expr + | LtacVarCall of Id.t * glob_tactic_expr + | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map + +type ltac_trace = (Loc.t * ltac_call_kind) list -- cgit v1.2.3 From ffac73b8f3f3bf6877ce652eecac7849b7c2a182 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 23:00:58 +0100 Subject: Moving Autorewrite to Hightatctic. --- intf/vernacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 7273b92b9a..5501ca7c7f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -69,7 +69,6 @@ type printable = | PrintHint of reference or_by_notation | PrintHintGoal | PrintHintDbName of string - | PrintRewriteHintDbName of string | PrintHintDb | PrintScopes | PrintScope of string -- cgit v1.2.3 From d868820ad1f00b896c5f44f18678fac2f8e0f720 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 13:18:10 +0100 Subject: Supporting "(@foo) args" in patterns, where "@foo" has no arguments. --- intf/constrexpr.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 40812a3d87..f5855a971e 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -40,15 +40,15 @@ type raw_cases_pattern_expr = | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t | RCPatCstr of Loc.t * Globnames.global_reference * raw_cases_pattern_expr list * raw_cases_pattern_expr list - (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) + (** [CPatCstr (_, c, l1, l2)] represents (@c l1) l2 *) | RCPatAtom of Loc.t * Id.t option | RCPatOr of Loc.t * raw_cases_pattern_expr list type cases_pattern_expr = | CPatAlias of Loc.t * cases_pattern_expr * Id.t | CPatCstr of Loc.t * reference - * cases_pattern_expr list * cases_pattern_expr list - (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) + * cases_pattern_expr list option * cases_pattern_expr list + (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) | CPatAtom of Loc.t * reference option | CPatOr of Loc.t * cases_pattern_expr list | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution -- cgit v1.2.3 From 3366f05ab09aa90dcc96d7432bff09617162c3e4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 17:49:25 +0100 Subject: Adopting the same rules for interpreting @, abbreviations and notations in patterns than in terms, wrt implicit arguments and scopes. See file Notations2.v for the conventions in use in terms. Somehow this could be put in 8.5 since it puts in agreement the interpretation of abbreviations and notations in "symmetric patterns" to what is done in terms (even though the interpretation rules for terms are a bit ad hoc). There is one exception: in terms, "(foo args) args'" deactivates the implicit arguments and scopes in args'. This is a bit complicated to implement in patterns so the syntax is not supported (and anyway, this convention is a bit questionable). --- intf/constrexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index f5855a971e..efd5129b66 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -40,7 +40,7 @@ type raw_cases_pattern_expr = | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t | RCPatCstr of Loc.t * Globnames.global_reference * raw_cases_pattern_expr list * raw_cases_pattern_expr list - (** [CPatCstr (_, c, l1, l2)] represents (@c l1) l2 *) + (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *) | RCPatAtom of Loc.t * Id.t option | RCPatOr of Loc.t * raw_cases_pattern_expr list -- cgit v1.2.3 From 25f39e54e4e8eaf08865121f06635dc3bd1092da Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 16 Feb 2016 21:17:12 +0100 Subject: Allowing generalized rules in typed symbols. --- intf/extend.mli | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/extend.mli b/intf/extend.mli index 57abdc38fb..e1520dec54 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -65,6 +65,17 @@ type user_symbol = (** {5 Type-safe grammar extension} *) +(** (a, b, r) adj => [a = x₁ -> ... xₙ -> r] & [b = x₁ * (... (xₙ * unit))]. *) +type (_, _, _) adj = +| Adj0 : ('r, unit, 'r) adj +| AdjS : ('s, 'b, 'r) adj -> ('a -> 's, 'a * 'b, 'r) adj + +type _ index = +| I0 : 'a -> ('a * 'r) index +| IS : 'a index -> ('b * 'a) index + +(** This type should be marshallable, this is why we use a convoluted + representation in the [Arules] constructor instead of putting a function. *) type ('self, 'a) symbol = | Atoken : Tok.t -> ('self, string) symbol | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol @@ -77,11 +88,19 @@ type ('self, 'a) symbol = | Anext : ('self, 'self) symbol | Aentry : 'a Entry.t -> ('self, 'a) symbol | Aentryl : 'a Entry.t * int -> ('self, 'a) symbol +| Arules : 'a rules -> ('self, 'a index) symbol -type ('self, _, 'r) rule = +and ('self, _, 'r) rule = | Stop : ('self, 'r, 'r) rule | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule +and 'a rules = +| Rule0 : unit rules +| RuleS : + ('any, 'act, Loc.t -> Loc.t * 'a) rule * + ('act, 'a, Loc.t -> Loc.t * 'a) adj * + 'b rules -> ((Loc.t * 'a) * 'b) rules + type 'a production_rule = | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule -- cgit v1.2.3 From ce2ffd090bd64963279cbbb84012d1b266ed9918 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 01:43:29 +0100 Subject: Moving VernacSolve to an EXTEND-based definition. --- intf/vernacexpr.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 5501ca7c7f..36b855ec3b 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -31,7 +31,6 @@ type goal_selector = | SelectNth of int | SelectId of Id.t | SelectAll - | SelectAllParallel type goal_identifier = string type scope_name = string @@ -363,7 +362,6 @@ type vernac_expr = (* Solving *) - | VernacSolve of goal_selector * int option * raw_tactic_expr * bool | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) -- cgit v1.2.3 From 0af598b77a6242d796c66884477a046448ef1e21 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 01:31:43 +0100 Subject: Moving Tactic Notation to an EXTEND based command. --- intf/vernacexpr.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 36b855ec3b..123b3ec1b7 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -291,8 +291,6 @@ type vernac_expr = | VernacError of exn (* always fails *) (* Syntax *) - | VernacTacticNotation of - int * grammar_tactic_prod_item_expr list * raw_tactic_expr | VernacSyntaxExtension of obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) -- cgit v1.2.3 From 01cd0dd64e4faa52b5094a99e2c31ecc4e7b767d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 02:09:54 +0100 Subject: Moving Print Ltac to an EXTEND based command. --- intf/vernacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 123b3ec1b7..1a67a37d7f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -60,7 +60,6 @@ type printable = | PrintClasses | PrintTypeClasses | PrintInstances of reference or_by_notation - | PrintLtac of reference | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions -- cgit v1.2.3 From 4f52bd681ad9bbcbbd68406a58b47d8e962336ed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 02:23:21 +0100 Subject: Moving the Ltac definition command to an EXTEND based command. --- intf/vernacexpr.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 1a67a37d7f..bd5890e296 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -379,7 +379,6 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of tacdef_body list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr -- cgit v1.2.3 From c4d62e3686926c27b172636ca8b746814d13a462 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 23:34:07 +0100 Subject: Moving type_uconstr to Pretyping. --- intf/tacexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index b1dc174d4b..0aa3b936ca 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -122,7 +122,7 @@ 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 'a delayed_open = +type 'a delayed_open = 'a Pretyping.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open -- cgit v1.2.3 From b3315a798edcaea533b592cc442e82260502bd49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 1 Apr 2016 11:13:07 +0200 Subject: Getting rid of the "_mods" parsing entry. It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations. --- intf/extend.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'intf') diff --git a/intf/extend.mli b/intf/extend.mli index e1520dec54..10713745e4 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -59,7 +59,6 @@ type user_symbol = | Ulist0 : user_symbol -> user_symbol | Ulist0sep : user_symbol * string -> user_symbol | Uopt : user_symbol -> user_symbol -| Umodifiers : user_symbol -> user_symbol | Uentry : string -> user_symbol | Uentryl : string * int -> user_symbol @@ -83,7 +82,6 @@ type ('self, 'a) symbol = | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol | Alist0sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol -| Amodifiers : ('self, 'a) symbol -> ('self, 'a list) symbol | Aself : ('self, 'self) symbol | Anext : ('self, 'self) symbol | Aentry : 'a Entry.t -> ('self, 'a) symbol -- cgit v1.2.3 From c6a8c4b5fa590f2beecd73817497bd7773a87522 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 10 Apr 2016 01:27:44 +0200 Subject: Expliciting the fact that the atomic tactic type is self-contained. --- intf/tacexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 0aa3b936ca..f821251c27 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -191,7 +191,7 @@ constraint 'a = < (** Possible arguments of a tactic definition *) -and 'a gen_tactic_arg = +type 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval | Reference of 'ref -- cgit v1.2.3 From 2da7bf6327e1f35321f121de9560604b758f0472 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 10 Apr 2016 02:37:41 +0200 Subject: Removing the ad-hoc tactic_expr type. This type was actually only used by the debug printer of tactics, and only for atomic tactics. Furthermore, that type was asymmetric, as the underlying tacexpr type was set to be glob_tactic, when the semantics would have required a Val.t type. Furthermore, this type is absent from every contrib I have seen, which hints again in favour of its lack of meaning. --- intf/tacexpr.mli | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index f821251c27..875ad3d160 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -377,19 +377,13 @@ type t_dispatch = < constant:t_cst; reference:t_ref; name:t_nam; - tacexpr:glob_tactic_expr; + tacexpr:unit; level:tlevel > -type tactic_expr = - t_dispatch gen_tactic_expr - type atomic_tactic_expr = t_dispatch gen_atomic_tactic_expr -type tactic_arg = - t_dispatch gen_tactic_arg - (** Misc *) type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen -- cgit v1.2.3 From 87a81fd7e6ff6b45c76690471eb671ba4b005338 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 Apr 2016 18:59:16 +0200 Subject: Moving and enhancing the grammar_tactic_prod_item_expr type. --- intf/vernacexpr.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 14a80379ec..ae9328fcc0 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -200,10 +200,6 @@ type one_inductive_expr = 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 - | TacNonTerm of Loc.t * string * (Names.Id.t * string) - type syntax_modifier = | SetItemLevel of string list * Extend.production_level | SetLevel of int -- cgit v1.2.3