aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
Changes: * Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive]; * Add ssrsetoid.v that links [ssrclasses.Reflexive] and [RelationClasses.Reflexive]; * Add [Require Coq.ssr.ssrsetoid] in Setoid.v; * Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that ports some non-exported material from rewrite.ml; * Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin; * Update doc and tests as well. Summary: * We can now use the under tactic in two flavors: - with the [eq] or [iff] relations: [Require Import ssreflect.] - or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.] (while [ssreflect] does not require [RelationClasses] nor [Setoid], and conversely [Setoid] does not require [ssreflect]). * The file ssrsetoid.v could be skipped when porting under to stdlib2.
2019-08-06[ssr] under: extend ssreflect.v to generalize iff to any setoid eqErik Martin-Dorel
* Add an extra test with an Equivalence. * Update the doc accordingly.
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-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
2019-06-13Integrate 8.9.0 and 8.9.1 changelog entries.Théo Zimmermann
From the CHANGES file in branch v8.9.
2019-06-12Merge PR #10310: Fix #10283: clearer dependency documentation for building ↵Clément Pit-Claudel
CoqIDE. Reviewed-by: cpitclaudel Reviewed-by: ejgallego
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic ↵Théo Zimmermann
definitions Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ggonthier Reviewed-by: herbelin
2019-06-09Merge PR #10245: Command line: adding variants for Require, aligning on the ↵Emilio Jesus Gallego Arias
vernac syntax Reviewed-by: cpitclaudel Reviewed-by: ejgallego Ack-by: herbelin
2019-06-08Mini fix documentation coqtop in passing.Hugo Herbelin
2019-06-08Documenting new options -require-import, -require-export, etc.Hugo Herbelin
Slight improving of style in passing.
2019-06-06Update changes.rst as a follow-up to #9743Kazuhiko Sakaguchi
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter.
2019-06-05Fix #10283: clearer dependency documentation for building CoqIDE.Théo Zimmermann
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-03Merge PR #10277: Remove Show Script (deprecated in 8.10)Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-28 08:13:58 +0000