diff options
Diffstat (limited to 'doc')
20 files changed, 153 insertions, 8 deletions
diff --git a/doc/changelog/02-specification-language/12653-cumul-syntax.rst b/doc/changelog/02-specification-language/12653-cumul-syntax.rst new file mode 100644 index 0000000000..ba97f7c796 --- /dev/null +++ b/doc/changelog/02-specification-language/12653-cumul-syntax.rst @@ -0,0 +1,5 @@ +- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now + support syntax `Inductive foo@{=i +j *k l}` to specify variance + information for their universes (in :ref:`Cumulative <cumulative>` + mode) (`#12653 <https://github.com/coq/coq/pull/12653>`_, by Gaëtan + Gilbert). diff --git a/doc/changelog/02-specification-language/13188-instance-gen.rst b/doc/changelog/02-specification-language/13188-instance-gen.rst new file mode 100644 index 0000000000..6a431f85ed --- /dev/null +++ b/doc/changelog/02-specification-language/13188-instance-gen.rst @@ -0,0 +1,6 @@ +- **Removed:** The type given to :cmd:`Instance` is no longer automatically + generalized over unbound and :ref:`generalizable <implicit-generalization>` variables. + Use :n:`Instance : \`{@type}` instead of :n:`Instance : @type` to get the old behaviour, or + enable the compatibility flag :flag:`Instance Generalized Output`. + (`#13188 <https://github.com/coq/coq/pull/13188>`_, fixes `#6042 + <https://github.com/coq/coq/issues/6042>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst b/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst new file mode 100644 index 0000000000..bf792fda6d --- /dev/null +++ b/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst @@ -0,0 +1,6 @@ +- **Added:** + Inference of return predicate of a :g:`match` by inversion takes + sort elimination constraints into account + (`#13290 <https://github.com/coq/coq/pull/13290>`_, + grants `#13278 <https://github.com/coq/coq/issues/13278>`_, + by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst new file mode 100644 index 0000000000..eaf049dc97 --- /dev/null +++ b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst @@ -0,0 +1,6 @@ +- **Fixed:** + A bug producing ill-typed instances of existential variables when let-ins + interleaved with assumptions + (`#13387 <https://github.com/coq/coq/pull/13387>`_, + fixes `#12348 <https://github.com/coq/coq/issues/13387>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst b/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst new file mode 100644 index 0000000000..048835a0e9 --- /dev/null +++ b/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst @@ -0,0 +1,6 @@ +- **Changed:** + Scope information is propagated in indirect applications to a + reference prefixed with :g:`@@`; this covers for instance the case + :g:`r.(@@p) t` where scope information from :g:`p` is now taken into + account for interpreting :g:`t` (`#12685 + <https://github.com/coq/coq/pull/12685>`_, by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst b/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst new file mode 100644 index 0000000000..089647a4b2 --- /dev/null +++ b/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Avoiding exposing an internal name of the form :n:`_tmp` when applying the + :n:`_` introduction pattern would break a dependency + (`#13337 <https://github.com/coq/coq/pull/13337>`_, + fixes `#13336 <https://github.com/coq/coq/issues/13336>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst b/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst new file mode 100644 index 0000000000..c02129a33f --- /dev/null +++ b/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst @@ -0,0 +1,6 @@ +- **Fixed:** + The case of tactics, such as :tacn:`eapply`, producing existential variables + under binders with an ill-formed instance + (`#13373 <https://github.com/coq/coq/pull/13373>`_, + fixes `#13363 <https://github.com/coq/coq/issues/13363>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst new file mode 100644 index 0000000000..a51f96d0a2 --- /dev/null +++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst @@ -0,0 +1,6 @@ +- **Deprecated:** + Undocumented :n:`eauto @int_or_var @int_or_var` syntax in favor of new ``bfs eauto``. + Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``; + replacement TBD. + (`#13381 <https://github.com/coq/coq/pull/13381>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst new file mode 100644 index 0000000000..1c7c3102a3 --- /dev/null +++ b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + :cmd:`Grab Existential Variables` and :cmd:`Existential` commands + (`#12516 <https://github.com/coq/coq/pull/12516>`_, + by Maxime Dénès). diff --git a/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst b/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst new file mode 100644 index 0000000000..74818f8464 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst @@ -0,0 +1,9 @@ +- **Changed:** + When compiled with OCaml >= 4.10.0, Coq will use the new best-fit GC + policy, which should provide some performance benefits. Coq's policy + is optimized for speed, but could increase memory consumption in + some cases. You are welcome to tune it using the ``OCAMLRUNPARAM`` + variable and report back setting so we could optimize more. + (`#13040 <https://github.com/coq/coq/pull/13040>`_, + fixes `#11277 <https://github.com/coq/coq/issues/11277>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst b/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst new file mode 100644 index 0000000000..8ec7198b72 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst @@ -0,0 +1,8 @@ +- **Deprecated:** + The default value for hint locality is currently :attr:`local` in a section and + :attr:`global` otherwise, but is scheduled to change in a future release. For the + time being, adding hints outside of sections without specifying an explicit + locality is therefore triggering a deprecation warning. It is recommended to + use :attr:`export` whenever possible + (`#13384 <https://github.com/coq/coq/pull/13384>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst new file mode 100644 index 0000000000..df2bdfeabb --- /dev/null +++ b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst @@ -0,0 +1,6 @@ +- **Changed:** + The :attr:`export` locality can now be used for all Hint commands, + including Hint Cut, Hint Mode, Hint Transparent / Opaque and + Remove Hints + (`#13388 <https://github.com/coq/coq/pull/13388>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/13365-axiom-free-wf.rst b/doc/changelog/10-standard-library/13365-axiom-free-wf.rst new file mode 100644 index 0000000000..1fc40894eb --- /dev/null +++ b/doc/changelog/10-standard-library/13365-axiom-free-wf.rst @@ -0,0 +1,4 @@ +- **Fixed:** + `Coq.Program.Wf.Fix_F_inv` and `Coq.Program.Wf.Fix_eq` are now axiom-free. They no longer assume proof irrelevance. + (`#13365 <https://github.com/coq/coq/pull/13365>`_, + by Li-yao Xia). diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 56d90b33d8..2474c784b8 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -391,6 +391,16 @@ Summary of the commands equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. + .. flag:: Instance Generalized Output + + .. deprecated:: 8.13 + + Disabled by default, this provides compatibility with Coq + version 8.12 and earlier. + + When enabled, the type of the instance is implicitly generalized + over unbound and :ref:`generalizable <implicit-generalization>` variables as though surrounded by ``\`{}``. + .. cmd:: Print Instances @reference Shows the list of instances associated with the typeclass :token:`reference`. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1fb337b30a..064107d088 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -246,6 +246,7 @@ The following is an example of a record with non-trivial subtyping relation: .. coqtop:: all Polymorphic Cumulative Record packType := {pk : Type}. + About packType. :g:`packType` binds a covariant universe, i.e. @@ -254,6 +255,27 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j +Specifying cumulativity +~~~~~~~~~~~~~~~~~~~~~~~ + +The variance of the universe parameters for a cumulative inductive may be specified by the user. + +For the following type, universe ``a`` has its variance automatically +inferred (it is irrelevant), ``b`` is required to be irrelevant, +``c`` is covariant and ``d`` is invariant. With these annotations +``c`` and ``d`` have less general variances than would be inferred. + +.. coqtop:: all + + Polymorphic Cumulative Inductive Dummy@{a *b +c =d} : Prop := dummy. + About Dummy. + +Insufficiently restrictive variance annotations lead to errors: + +.. coqtop:: all + + Fail Polymorphic Cumulative Record bad@{*a} := {p : Type@{a}}. + An example of a proof using cumulativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -280,7 +302,7 @@ An example of a proof using cumulativity End down. Cumulativity Weak Constraints ------------------------------ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. flag:: Cumulativity Weak Constraints @@ -383,6 +405,7 @@ Explicit Universes | _ | @qualid univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} + cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} univ_constraint ::= @universe_name {| < | = | <= } @universe_name The syntax has been extended to allow users to explicitly bind names diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index d3bd787587..ad7d6f3963 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -8,13 +8,14 @@ Inductive types .. cmd:: Inductive @inductive_definition {* with @inductive_definition } - .. insertprodn inductive_definition constructor + .. insertprodn inductive_definition cumul_ident_decl .. prodn:: - inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } + inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } + cumul_ident_decl ::= @ident {? @cumul_univ_decl } This command defines one or more inductive types and its constructors. Coq generates destructors diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index e6dc6f6c51..cc4ab76502 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -123,6 +123,10 @@ Programmable proof search .. example:: + .. coqtop:: none + + Set Warnings "-deprecated-hint-without-locality". + .. coqtop:: all Hint Resolve ex_intro : core. @@ -280,13 +284,18 @@ automatically created. sections. + :attr:`export` are visible from other modules when they import the current - module. Requiring it is not enough. This attribute is only effective for - the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and - :cmd:`Hint Extern` variants of the command. + module. Requiring it is not enough. + :attr:`global` hints are made available by merely requiring the current module. + .. deprecated:: 8.13 + + The default value for hint locality is scheduled to change in a future + release. For the time being, adding hints outside of sections without + specifying an explicit locality is therefore triggering a deprecation + warning. It is recommended to use :attr:`export` whenever possible + The various possible :production:`hint_definition`\s are given below. .. cmdv:: Hint @hint_definition @@ -407,6 +416,10 @@ automatically created. .. example:: + .. coqtop:: none + + Set Warnings "-deprecated-hint-without-locality". + .. coqtop:: in Hint Extern 4 (~(_ = _)) => discriminate : core. @@ -421,7 +434,11 @@ automatically created. .. example:: - .. coqtop:: reset all + .. coqtop:: reset none + + Set Warnings "-deprecated-hint-without-locality". + + .. coqtop:: all Require Import List. Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index fd8a0329d6..40d032543f 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -288,12 +288,18 @@ Name a set of section hypotheses for ``Proof using`` existential variables remain. To instantiate existential variables during proof edition, you should use the tactic :tacn:`instantiate`. + .. deprecated:: 8.13 + .. cmd:: Grab Existential Variables This command can be run when a proof has no more goal to be solved but has remaining uninstantiated existential variables. It takes every uninstantiated existential variable and turns it into a goal. + .. deprecated:: 8.13 + + Use :cmd:`Unshelve` instead. + Proof modes ``````````` diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index a787d769fb..033ece04de 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1623,6 +1623,7 @@ simple_tactic: [ | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "dfs" "eauto" OPT int_or_var auto_using hintbases +| "bfs" "eauto" OPT int_or_var auto_using hintbases | "autounfold" hintbases clause_dft_concl | "autounfold_one" hintbases "in" hyp | "autounfold_one" hintbases diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 26474d950a..dfd3a18908 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -434,6 +434,10 @@ univ_decl: [ | "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" ] +cumul_univ_decl: [ +| "@{" LIST0 ( OPT [ "=" | "+" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" +] + univ_constraint: [ | universe_name [ "<" | "=" | "<=" ] universe_name ] @@ -695,7 +699,7 @@ field_def: [ ] inductive_definition: [ -| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations +| OPT ">" cumul_ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations ] constructors_or_record: [ @@ -707,6 +711,10 @@ constructor: [ | ident LIST0 binder OPT of_type ] +cumul_ident_decl: [ +| ident OPT cumul_univ_decl +] + filtered_import: [ | qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ] ] @@ -1754,6 +1762,7 @@ simple_tactic: [ | "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases | "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases | "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases +| "bfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases | "autounfold" OPT hintbases OPT clause_dft_concl | "autounfold_one" OPT hintbases OPT ( "in" ident ) | "unify" one_term one_term OPT ( "with" ident ) |