aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-12-30Merge PR #13684: Document the -native-compiler optioncoqbot-app[bot]
Reviewed-by: silene Ack-by: Zimmi48 Ack-by: jfehrle
2020-12-29[refman] Clarify meaning of goal in documentation of instantiate.Théo Zimmermann
2020-12-29Document the -native-compiler optionPierre Roux
2020-12-28Merge PR #13665: Set Python's default output encoding to utf-8coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: palmskog
2020-12-26Set the locale in Docker so Python's default output encoding is utf-8Jim Fehrle
2020-12-21Shorten/improve intro of "Basic proof writing" chapter.Théo Zimmermann
2020-12-16Merge PR #13643: Add -q flag to coqrst python invocation of coqtopcoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2020-12-16Add -q flag to coqrst python invocation of coqtopLasse Blaauwbroek
This will help with reproducibility for people who have something in their coqrc file. Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ↵Pierre-Marie Pédrot
tactics. Reviewed-by: ppedrot
2020-12-14Adding change log for #13568.Hugo Herbelin
2020-12-14Merge PR #13613: [changes] mark #12765 as experimentalcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-14Merge PR #13509: Remove compatibility flag Set Bracketing Last Introduction ↵Pierre-Marie Pédrot
Pattern Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-12-13Merge PR #13619: doc: Clarify the status of simpl vs cbncoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-13Add changelog for #13509.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-12-11doc: Clarify the status of simpl vs cbnClément Pit-Claudel
The cbn tactic was documented in aa9db490a2. The current manual causes confusion by suggesting that cbn is a replacement for simpl, while in practice they do different things, both with their own quirks. Given that neither is consistently faster than the other, I think it's worth clarifying the manual.
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral ↵coqbot-app[bot]
notations. Reviewed-by: jfehrle Reviewed-by: proux01 Ack-by: Zimmi48 Ack-by: SkySkimmer
2020-12-11Merge PR #13611: Clarify changelog categories.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-12-11Merge PR #13612: Bump reference to 8.12 refman following unexpected 8.12.2 ↵Clément Pit-Claudel
release. Reviewed-by: cpitclaudel
2020-12-11Merge PR #13582: Generalize exp_ineq1 and add exp_ineq1_le, which holds ↵coqbot-app[bot]
forall Reals. Reviewed-by: thery
2020-12-11[changes] mark #12765 as experimentalEnrico Tassi
2020-12-11Bump reference to 8.12 refman following unexpected 8.12.2 release.Théo Zimmermann
2020-12-11Clarify changelog categories.Théo Zimmermann
For readers of the changelog: title "Tools" become "Command-line tools". For developers: changelog categories 07 and 08 are disambiguated.
2020-12-10Changelog for 8.12.2.Théo Zimmermann
2020-12-09Merge PR #13564: Allow all characters in tacn, cmd, ... names. Report ↵Clément Pit-Claudel
duplicate names. Ack-by: Zimmi48 Reviewed-by: cpitclaudel
2020-12-09Allow any character in a tacn, cmd, ... nameJim Fehrle
Include "0-9_" in default cmd name Report duplicate names
2020-12-09Redefines exp_ineq1 to hold for all non-zero numbers.Avi Shinnar
The original (which holds only for positive numbers) is now called exp_ineq1_pos. A version that holds only for negative numbers is added as exp_ineq1_neg. Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). Co-authored-by: Barry M. Trager <bmt@us.ibm.com>
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-12-06[doc] update changes after 13501Enrico Tassi
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-05Merge PR #13553: Document Number Notation for primitive integerscoqbot-app[bot]
Reviewed-by: jfehrle
2020-12-04Merge PR #13569: typocoqbot-app[bot]
Reviewed-by: jfehrle
2020-12-04Merge PR #13442: Add an abstraction function in the LtacX FFI.coqbot-app[bot]
Reviewed-by: kyoDralliam
2020-12-04typoYves Bertot
2020-12-04Merge PR #13527: Changes for Coq 8.13coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API) - the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors - Grants #13484: String notations for primitive arrays - Fixes #13517: String notation printing fails with primitive integers inside lists
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:02:37 +0000