| Age | Commit message (Collapse) | Author |
|---|
|
We deprecate unspecified locality as was done for Hint.
Close #13724
|
|
|
|
The Detailed examples of tactics chapter can be removed when the
remaining examples are moved closer to the definitions of the
corresponding tactics.
This commit also moves back the footnotes from the Tactics chapter at
the end of the chapter, and removes an old footnote that doesn't
matter anymore.
|
|
By default Coq warnings are made fatal when building the manual.
If you want to show a command resulting in a warning, use the warn
option.
Preexisting warnings are either fixed or marked as expected.
|
|
|
|
As far as I know, this plugin is untested and barely maintained. I don't
think it has real use cases any more, so let's move it out from the repo
and see if somebody wants to take over and maintain it.
We also remove the documentation, which was telling our users to look at
ring to see an example of reification done using quote, when in fact it
wasn't using it anymore.
|
|
|
|
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
|
|
Most existing uses of .. example did not use the first line as a title, so this
commit also adds appropriate blank lines.
|
|
|
|
tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged.
|
|
the formatting and renamed the tactics to match modern naming conventions.
|
|
Manual.
|
|
|
|
Including cross-reference TODOs.
I took down the number of warnings from 300 to 50.
|
|
Thanks to Calvin Beck for porting this chapter.
|
|
|
