| Age | Commit message (Collapse) | Author |
|---|
|
Was PR#350: tclDISPATCH: more informative error message
|
|
|
|
This was not fixed by b9a15a390f yet.
|
|
This commit uses the proper url for bug reporting, marks urls as such,
stops qualifying the Coq'Art book as new, and fix the spacing after the
Coq name.
|
|
cofixpoint (bug #5286).
|
|
The way \zeroone was defined, the \tt modifier was leaked outside the
brackets, thus messing with the following text. There are a bunch of
occurrences of this issue in the manual, so rather than turning all the
\tt into \texttt, the definition of \zeroone is made more robust.
Unfortunately, there is one single occurrence of \zeroone that does not
support the more robust version. (Note that this specific usage of
\zeroone is morally a bug, since it goes against all the LaTeX
conventions.) So the commit also keeps the old leaky version of \zeroone
around as \zeroonelax so that it can be used there.
|
|
|
|
|
|
|
|
|
|
cofixpoint (bug #5286).
|
|
This is only a quick fix, as hinted by Jason.
|
|
This also fixes decide equality, discriminate, ... (see e.g. #5279).
|
|
|
|
Was PR#172: alternate path separators in typeclass debug output.
|
|
Make does not allow for rules that produce multiple outputs (unless they
are pattern rules). As a consequence, the hacha rule could be run several
times concurrently, thus causing doc/refman/html to be deleted under the
feet of some runs.
This commit fixes the issue by turning the rule into a single-output rule
and adding a dummy rule to handle all the other indexes. Note that this is
not a perfect solution since, if the user were to manually delete one of
the auxiliary index, it would not be rebuilt until the main index is.
|
|
Was PR#351: Complete a truncated comment
|
|
Was PR#363: lib/Unicodetable: Update.
|
|
|
|
Was decided during the working group on September, 28th.
|
|
|
|
|
|
- Add a debug message when applying a heuristic.
- Fix double newlines.
|
|
This is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial
changes in the other files, the real changes are in the parent commit.
|
|
This brings the fix in cad44fc for #2996 to the copy of
Fast_typeops.check_hyps_inclusion.
Fast_typeops.constant_type checks the universe constraints instead of
outputting them. Since everyone who used Typeops.constant_type just
discarded the constraints they've been switched to constant_type_in
which should be the same in Fast_typeops and Typeops.
There are some small differences in the interfaces:
- Typeops.type_of_projection <->
Fast_typeops.type_of_projection_constant to avoid collision with the
internally used type_of_projection (which gives the type of [Proj(p,c)]).
- check_hyps_inclusion takes [('a -> constr)] and ['a] instead of
[constr] for reporting errors.
|
|
because P:U->Prop implies P:U->Type, the new statement is strictly more useful.
No change was needed to the proof.
|
|
|
|
|
|
|
|
The sad part of the story is that the script testing this version number
is run after tagging by the coq-dev-tools Makefile... will fix that.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This was yet another bug in the VM long multiplication, that
I unfortunately introduced in ebc509ed2. It was impacting only 32-bit
architectures.
In the future, I'll try to make sure that
1) we provide unit tests for integer arithmetic (my int63 branch ships
with such tests)
2) our continuous testing infrastructure runs the test suite on a 32-bit
architecture. I tried to set up such an instance, but failed. Waiting
for support reply.
|
|
The way \zeroone was defined, the \tt modifier was leaked outside the
brackets, thus messing with the following text. There are a bunch of
occurrences of this issue in the manual, so rather than turning all the
\tt into \texttt, the definition of \zeroone is made more robust.
Unfortunately, there is one single occurrence of \zeroone that does not
support the more robust version. (Note that this specific usage of
\zeroone is morally a bug, since it goes against all the LaTeX
conventions.) So the commit also keeps the old leaky version of \zeroone
around as \zeroonelax so that it can be used there.
|
|
|
|
Was PR#387: ssrmatching: handle primitive projections (fix: #5247)
|
|
Was PR#389: Changed mention of deprecated -byte option to .byte suffix;
change module for Coq loop
|
|
|
|
|
|
|
|
Some C files included in build scripts (in dev/build) were triggering
errors or warnings on non-win32 platforms.
Note that ide/ide_win32_stubs.c was already handled through an ad-hoc
rule in Makefile.
If you add a new C file outside of kernel/byterun, please extend the CFILES
variable.
|
|
Richpp output depends on printing width, thus its internal formatter
should be seeded with the proper width value.
While we are at it, we increase the default buffer size to a more
sensible value.
|
|
Was PR#366: Univs: fix bug 5208
|
|
Was PR#378: Univs: fix bug #5188
|
|
|
|
|
