From 1a43fda0dc9bb8d100808426980446353f8f1ae3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Apr 2017 11:21:23 +0200 Subject: Removing internal support for accepting "{struct x}" and co in "Theorem with". There were actually no syntax for it, and I'm still unsure what good syntax to give to it, even more that it would be useful to have one. --- 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 25d3c705f4..d62c639c2e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -209,7 +209,7 @@ type one_inductive_expr = plident * local_binder_expr list * constr_expr option * constructor_expr list type proof_expr = - plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option) + plident option * (local_binder_expr list * constr_expr) type syntax_modifier = | SetItemLevel of string list * Extend.production_level -- cgit v1.2.3 From 8d69323dff6e1afd17a13dfa8a980e76acb44cdc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Apr 2017 15:53:35 +0200 Subject: Documenting how the recursive indices of a fixpoint are computed. Also documenting how the implicit arguments by position are computed. --- 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 49bafadc8e..a4a6eb9092 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -19,7 +19,7 @@ open Decl_kinds type notation = string type explicitation = - | ExplByPos of int * Id.t option + | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *) | ExplByName of Id.t type binder_kind = -- cgit v1.2.3 From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:11:47 +0200 Subject: Remove unused [open] statements --- intf/tactypes.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'intf') diff --git a/intf/tactypes.mli b/intf/tactypes.mli index 02cfc44e29..ef90b911c5 100644 --- a/intf/tactypes.mli +++ b/intf/tactypes.mli @@ -13,7 +13,6 @@ open Loc open Names open Constrexpr -open Glob_term open Pattern open Misctypes -- cgit v1.2.3 From 7943b1fade775af48917d54878e65b80217be038 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 28 Apr 2017 16:15:10 +0200 Subject: Using a more explicit algebraic type for evars of kind "MatchingVar". A priori considered to be a good programming style. --- intf/evar_kinds.mli | 5 ++++- intf/glob_term.mli | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) (limited to 'intf') diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index 470ad2a23b..75dad2e918 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -8,6 +8,7 @@ open Names open Globnames +open Misctypes (** The kinds of existential variable *) @@ -16,6 +17,8 @@ open Globnames type obligation_definition_status = Define of bool | Expand +type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar + type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) @@ -27,6 +30,6 @@ type t = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase - | MatchingVar of bool * Id.t + | MatchingVar of matching_var_kind | VarInstance of Id.t | SubEvar of Constr.existential_key diff --git a/intf/glob_term.mli b/intf/glob_term.mli index ced5a8b44f..ba4a47a365 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -38,7 +38,7 @@ type glob_constr = (** 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 *) + | GPatVar of Loc.t * Evar_kinds.matching_var_kind (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr -- cgit v1.2.3 From 4f742e14441581ece247d33020055f15732f126b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 28 Apr 2017 22:14:09 +0200 Subject: Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"." I'm sure this was pushed by accident, since testing shows immediately that it breaks the compilation of the ssreflect plugin, hence all developments relying on it in Travis. --- intf/evar_kinds.mli | 5 +---- intf/glob_term.mli | 2 +- 2 files changed, 2 insertions(+), 5 deletions(-) (limited to 'intf') diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index 75dad2e918..470ad2a23b 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -8,7 +8,6 @@ open Names open Globnames -open Misctypes (** The kinds of existential variable *) @@ -17,8 +16,6 @@ open Misctypes type obligation_definition_status = Define of bool | Expand -type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar - type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) @@ -30,6 +27,6 @@ type t = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase - | MatchingVar of matching_var_kind + | MatchingVar of bool * Id.t | VarInstance of Id.t | SubEvar of Constr.existential_key diff --git a/intf/glob_term.mli b/intf/glob_term.mli index ba4a47a365..ced5a8b44f 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -38,7 +38,7 @@ type glob_constr = (** 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 * Evar_kinds.matching_var_kind (** Used for patterns only *) + | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr -- cgit v1.2.3 From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Thu, 6 Apr 2017 22:48:32 +0200 Subject: Allow flexible anonymous universes in instances and sorts. The addition to the test suite showcases the usage. --- 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 33dc2a335c..7c2dc5177c 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -48,8 +48,8 @@ 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 +type sort_info = Name.t Loc.located list +type level_info = Name.t Loc.located option type glob_sort = sort_info glob_sort_gen type glob_level = level_info glob_sort_gen -- cgit v1.2.3 From b643916aed4093eb7f21116aaef726cab561bc27 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 15 May 2017 01:10:54 +0200 Subject: [interp] [ast] Make raw_cases_pattern_expr private. The type `raw_cases_pattern_expr` is used only in the interpretation of notation patterns. Indeed, this should be a private type thus we make it local to `Constrintern`; it makes no sense to expose it in the public AST. The patch is routine, except for the case used to interpret primitives in patterns. We now return a `glob_constr` representing the raw pattern, instead of the private raw pattern type. This could be further refactored but have opted to be conservative here. This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754 , see the commentaries there for more information about `raw_cases_pattern_expr`. --- intf/constrexpr.mli | 8 -------- 1 file changed, 8 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index a4a6eb9092..77f052ddbd 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -36,14 +36,6 @@ 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 - | 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) *) - | RCPatAtom of Loc.t * Id.t option - | RCPatOr of Loc.t * raw_cases_pattern_expr list - type instance_expr = Misctypes.glob_level list type cases_pattern_expr = -- cgit v1.2.3 From c1e9a27d383688e44ba34ada24fe08151cb5846e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 17 May 2017 21:04:18 +0200 Subject: [vernac] Remove `Save thm id.` command. We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc... --- intf/vernacexpr.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index cb093d85d5..94fa37eb69 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -143,6 +143,7 @@ type search_restriction = type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) + (* list of idents for qed exporting *) type opacity_flag = Opaque of lident list option | Transparent type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option @@ -223,7 +224,8 @@ type syntax_modifier = type proof_end = | Admitted - | Proved of opacity_flag * (lident * theorem_kind option) option + (* name in `Save ident` when closing goal *) + | Proved of opacity_flag * lident option type scheme = | InductionScheme of bool * reference or_by_notation * sort_expr -- cgit v1.2.3