| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.
|
|
A commit at 2003-03-13 changed the lemma name.
https://github.com/coq/coq/commit/cb1ae314411d78952062e5092804b85d981ad6e1
|
|
|
|
This is a companion to #12479 as per
https://github.com/coq/coq/pull/12479#issuecomment-641336039 that
changes some of the PrimFloat notations:
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
We also put them in a module, so users can `Require PrimFloat. Import
PrimFloat.PrimFloatNotations` without needing to unqualify the
primitives.
Fixes the part of #12454 about floats
|
|
|
|
|
|
|
|
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
|
|
|
|
|
|
|
|
for integers and natural nums
|
|
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.
|
|
|
|
Mostly in the pattern
~~~
.. coqtop:: in
Theorem foo : bla.
Theorem bar : blah. (* nested proof error *)
~~~
|
|
|
|
And a few more Sphinx fixes in passing.
|
|
Mark boolean-valued options with :flag:
Adjust tactic and command names so parameters aren't shown in the index unless
they're needed for disambiguation.
Remove references to synchronous options.
Revise doc for tables.
Correct indentation for text below :flag:
|
|
|
|
Most existing uses of .. example did not use the first line as a title, so this
commit also adds appropriate blank lines.
|
|
of the Reference Manual.
|
|
Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes.
|
|
As stated in the manual, the fourier tactic is subsumed by lra.
|
|
Including adding missing irrefutable-patterns to the grammar of binders.
|
|
|
|
Including cross-reference TODOs.
I took down the number of warnings from 300 to 50.
|
|
These were used very inconsistenty, serve no purpose and the link
to the source is particularly useless because it's a moving target.
|
|
Thanks to Pierre Letouzey for porting this chapter.
|
|
|
