| Age | Commit message (Collapse) | Author |
|---|
|
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
|
|
A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing
a matching over a "catch-all" variable, when let-ins occur in the
arity. However ade2363e35 failed to understand what was the correct
fix, introducing instead the regressions mentioned in #5322 and #5324.
This fixes all of #5322 and #5324, as well as the handling of let-ins
in the arity.
Thanks to Jason for helping in diagnosing the problem.
|
|
This reverts commit 1d4c34c79624fb81e64dfed8874b2fc9fa66c070.
It seems the proof terminator of obligation.ml, in the case in which
Set Shrink Obligation is set, accesses the opaque proof.
|
|
|
|
This was observable in long proofs, because side effects kept being
duplicated, leading to an additional cost linear in the size of the proof.
This commit touches kernel files, but the corresponding API is only used
in tactic-facing code so that the side_effects type remains opaque. Thus
it does not affect the kernel safety.
|
|
|
|
This was deactivated by 27c9346 and made an optimization moot in eauto. This
optimization was physically checking for equality, but as lists where rebuilt
by the mapping, this was never true. Some contribs were thus quite slower,
including persistent-union-find which was twice slower.
This 2-line patch fixes it by trying to preserve sharing as much as possible.
Note that we should still do something about eauto, because it does redo
useless work a lot whenever the environment only changes a bit, while we could
cache this computation.
|
|
|
|
- We fix the inconsistency of Structure and Record which according to
doc are the same.
- We improve the error message when not using { ... } for Record or Structure.
|
|
The same file name for .dot graphs could be used by concurrent processes.
|
|
The aux file for foo/bar.v is foo/.bar.aux, not .foo/bar.aux.
|
|
Coq expects aux_file_name_for to give the aux file corresponding to the
input file whichever its Coq-related extension, be it .v or .vo or .vio.
Commit 3e6fa1c broke this contract when fixing bug #5183. As a
consequence, depending on the execution path, Coq would try to save or
load from either .foo.aux or .foo.vo.aux or .foo.vio.aux.
This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call
chain by not initializing hints when the input file does not end with .v.
This also restores 8.5 behavior with respect to aux file naming.
|
|
#5307).
|
|
|
|
Addition of debug info can be prevented using -nodebug at configure
time.
|
|
|
|
We did not decide precisely what minor version we would support, so
relaxing. We document why 4.02.0 is not supported (its use is also
discouraged by the OCaml team, see e.g. https://ocaml.org/releases/).
|
|
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.
|
|
|
|
|
|
|
