aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-12-03Implement review corrections by Théo ZimmermannMatthieu Sozeau
2020-12-03Implement suggestions by Théo ZimmermannMatthieu Sozeau
2020-12-03Apply suggestions from code reviewMatthieu Sozeau
Co-authored-by: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-12-03Apply suggestions from code reviewEnrico Tassi
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Update doc/sphinx/changes.rstMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Fixes in the summary by Jim FehrleMatthieu Sozeau
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-12-03Changes without PR references fixesMatthieu Sozeau
2020-12-03Apply suggestions from @jfehrle code reviewMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Add an anchor in syntax-extensionsMatthieu Sozeau
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-12-03[refman] Fix error names.Théo Zimmermann
The @ syntax is not supported in the name, so we transform it manually as it would have been if no name had been provided.
2020-12-03Merge PR #13554: Split long lines in errors and warning indexcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-02Split long lines in errors and warning indexJim Fehrle
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Document Number Notation for primitive integersPierre Roux
2020-12-02Put all Int63 primitives in a separate filePierre Roux
Following a request from Pierre-Marie Pédrot in #13258
2020-12-01Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0coqbot-app[bot]
Reviewed-by: gares
2020-11-30Adding a changelog for Ltac1.lambda.Pierre-Marie Pédrot
2020-11-30Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for ↵coqbot-app[bot]
cumulative inductive types Reviewed-by: SkySkimmer
2020-11-29Backport ssrbool lemmas from MathComp 1.12.0Kazuhiko Sakaguchi
2020-11-28Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."coqbot-app[bot]
Reviewed-by: gares
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: herbelin Ack-by: jfehrle
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ↵Matthieu Sozeau
types
2020-11-27Merge PR #13483: Fix #13283: improved error on `clear implicit` flagcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
2020-11-27Merge PR #13482: Improved error message on nested proofscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: gares Ack-by: jfehrle
2020-11-27Merge PR #13473: Testing {in _, _} and {pred _} from ssrboolcoqbot-app[bot]
Reviewed-by: gares
2020-11-27Improved error message on nested proofsFabian Kunze
to include most common reason when this happens on accident
2020-11-27Fix #13283: improved error on `clear implicit` flagFabian Kunze
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
As discussed in the Coq meeting.
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks.
2020-11-26[declare] Allow custom typing flags when declaring constants.Emilio Jesus Gallego Arias
We use the new `Declare.Info` structure to uniformly add properties to the handling of constants. In this case, per-constant typing flags. The internal code may want to see some further refactoring, including pushing the flags down to `Safe_typing.add_constant` , but the changes in the interface should be definitive. This will allow #12539 and #9004 using attributes.
2020-11-25Testing {in _, _} and {pred _} from ssrboolCyril Cohen
2020-11-25Changelog for #13415Gaëtan Gilbert
2020-11-25Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bugcoqbot-app[bot]
Reviewed-by: gares
2020-11-25Merge PR #13405: Alternative implementation of the Micromega persistent cacheVincent Laporte
Reviewed-by: vbgl
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-24Add a changelog.Pierre-Marie Pédrot
2020-11-24Fixing [dup] and [swap]Cyril Cohen
2020-11-23Add COPYALL and APPENDALL edit ops, drop unneeded codeJim Fehrle
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term ↵coqbot-app[bot]
notations. Reviewed-by: jfehrle Reviewed-by: gares Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make ↵coqbot-app[bot]
sense Reviewed-by: Zimmi48
2020-11-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
For constr, this means clarifying that "ident" is deprecated and to be replaced by "name". Here, some cleaning shall have to be done at the end of deprecation phase, when "ident" will take its literal meaning. For custom notations, this is about documenting the effect of "ident" and "global" which was yet undocumented. Note that we anticipate an example in constr working with the literal meaning of "ident" (temporarily silencing the warning). Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
We use a deprecation phase where: - "ident" means "name" (as it used to mean), except in custom coercion entries where it already meant "ident". - "ident" will be made again available (outside situation of coercions) to mean "ident" at the end of deprecation phase. Also renaming "as ident" into "as name". Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the ↵Pierre-Marie Pédrot
same time (granting #9816) Reviewed-by: Zimmi48 Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:36:46 +0000