aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2019-09-16Re-implementation of zifyFrédéric Besson
The logic is implemented in OCaml. By induction over the terms, guided by registered Coq terms in ZifyInst.v, it generates a rewriting lemma. The rewriting is only performed if there is some progress. If the rewriting fails (due to dependencies), a novel hypothesis is generated. This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848 ans fixes #10755. The zify plugin is placed in the micromega directory. (Though the reason is unclear, having it in a separate directory is bad for efficiency.) efficiency impact. There are also a few improvements of lia/lra that are piggybacked. - more aggressive pruning of useless hypotheses - slightly optimised conjunctive normal form - applies exfalso if conclusion is not in Prop - removal of Timeout in test-suite
2019-09-12Merge PR #10753: Release notes for 8.10+beta3.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-09-12Release notes for 8.10+beta3.Théo Zimmermann
2019-09-10Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely.Hugo Herbelin
2019-09-10Fixing coqide doc about location of "coqiderc" and "coqide.bindings".Hugo Herbelin
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
Fix changelog entry Fix build of the user manual Markup fixes from Théo Zimmermann Update doc and changelog and improve error messages.
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
This improves error reporting. Addendum to #10515
2019-08-23[doc] Fix documentation of schedule-vioEmilio Jesus Gallego Arias
Master version of the fix for #10679
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations ↵Maxime Dénès
involving & Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Ack-by: ggonthier Ack-by: herbelin Reviewed-by: maximedenes Ack-by: vbgl
2019-08-05Merge PR #10624: Remove reference to removed option Printing Primitive ↵Théo Zimmermann
Projection Compatibility Reviewed-by: Zimmi48
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-29Document changes by PR 10324Vincent Laporte
White spaces are forbidden in the “&ident” syntax for ltac2 references.
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel Ack-by: herbelin
2019-07-29Merge PR #10574: Remove deprecated `Backtrack` commandEnrico Tassi
Reviewed-by: ejgallego Reviewed-by: gares
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
for integers and natural nums
2019-07-26Remove the tactic wizard, as it has not worked for several years and no one ↵Guillaume Melquiond
complained (fixes #10580).
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
It has been deprecated since 8.4. The documentation was incorrect since at least 8.5 (the last two arguments were ignored). `Backtrack m n p` was a synonym for `BackTo m` We also move `BackTo` handling to coqtop, since it is not meant to be part of the document.
2019-07-23doc: Fix a detail in 2 files describing the under tacticErik Martin-Dorel
href: coq/coq#9651
2019-07-22[Int63] Implement all primitives in OCamlVincent Laporte
Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are implemented in the kernel so that they can be used by OCaml code (e.g., extracted code) as the other primitives.
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
The ExtrOCamlInt63 module can be required to map primitives from the Int63 module to their OCaml implementation (module Uint63 from the kernel).
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: mattam82
2019-07-18[doc] Fix typo in doc/sphinx/addendum/ring.rstWojciech Nawrocki
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-11Merge PR #10424: Update doc for % escapes in Sphinx, improve error messagesClément Pit-Claudel
Reviewed-by: cpitclaudel
2019-07-11Update doc/sphinx/proof-engine/ssreflect-proof-language.rstFlorent Hivert
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-07-10Fixed a few wrong reference and typosFlorent Hivert
2019-07-05Correct doc about default value for Typeclasses Dependency OrderGaëtan Gilbert
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ↵Kazuhiko Sakaguchi
new one
2019-07-01Update doc for % escapes in Sphinx doc, improve error messagesJim Fehrle
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: herbelin Ack-by: jfehrle
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
It prints a goal given its internal goal id and the Stm state id.
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
This looks more principled, and doesn't require as much tinkering with the typing implementation.
2019-06-25Documenting the Ltac2 change.Pierre-Marie Pédrot
2019-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations ↵Théo Zimmermann
in favor of "simple_intropattern" Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-06-17Merge PR #10392: Fix the changelog of 8.10+beta2 following the backport of ↵Clément Pit-Claudel
#10205. Reviewed-by: cpitclaudel
2019-06-17Fix the changelog of 8.10+beta2 following the backport of #10205.Théo Zimmermann
2019-06-17Update copyright years outside of headers.Théo Zimmermann
These were found with the following command: $ git grep "1999-" | grep -v "2019"
2019-06-17Adapt change-header script to handle shebangs in addition to Emacs comments.Théo Zimmermann
Remove other types of lines before copyright headers.
2019-06-17Update c-style headers to new year.Théo Zimmermann
2019-06-16Changelog for 8.10+beta2.Théo Zimmermann
2019-06-16Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".Hugo Herbelin
This is to prevent confusion with the terminology used in the grammar of tactic in the reference manual: "intropattern" in Tactic Notation and TACTIC EXTEND is actually bound to simple_intropattern and not to what is called intropattern in the reference manual After some deprecation phase, "intropattern" could be added back to mean the "intropattern" of the reference manual. Note that "simple_intropattern" is actually already available in "Tactic Notation" with the correct meaning as an entry. Only "intropattern" is misguiding.
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
This allows to refer to them from other part of the manual without any ambiguity.
2019-06-14Merge PR #10322: Update changes.rst as a follow-up to #9743Théo Zimmermann
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 20:28:16 +0000