| Age | Commit message (Collapse) | Author |
|---|
|
It will be possible to replace any call to 'autounfoldify x' with 'autounfold with x'.
|
|
The use case is to take a hint database as an argument of Ltac or Tactic Notation.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
iris-coq math-classes sf
- [TLC] [metacoq] not ready for 8.6 yet
|
|
|
|
- Add README.ci
Suggestions and comments welcome.
- Use the system compiler to get some boot speedup.
- Build log folding.
- Set NJOBS=2 (very moderate speedup)
- Set language to a defined value.
OPAM itself recommends C, so we follow suit.
- Remove spurious `.opam`test
No harm in testing we are in the right opam setting even if the
cache did exist.
Anyways, it seems that the previous was spurious, as it was testing
if ~/coq/.opam did exists. I think the correct command would have
been:
```shell
[ -e ${HOME}/.opam ] || opam init ...
```
See the log at https://travis-ci.org/coq/coq/builds/198948812 for an
example.
|
|
- Improve the setup to support external contribs.
We use a more minimalistic Coq build, gaining a few extra minutes.
- [math-comp] workaround `make -j` bug to enable parallel building.
|
|
We also optimize `travis_wait` use.
|
|
|
|
|
|
|
|
Commits were squashed.
|
|
|
|
|
|
|
|
This was introduced in 8.5 while reorganizing the structure of
intro-patterns.
|
|
|
|
|
|
|
|
|
|
|
|
This is a modest contribution serving before all the purpose of
displaying the focus stack and the shelf and give_up list. It does not
print the sigma (while it could).
Any improvements are welcome.
|
|
The native compiler doesn't support `Require` inside `Module` sections
in some cases, we improve the error message. See:
https://coq.inria.fr/bugs/show_bug.cgi?id=4335
This patch improves the error message and gives the user some
feedback.
|
|
We complete the support of 'pat in this particular case (a 'pat under
a binder in a notation).
|
|
|
|
|
|
Tracking conversion problems to reconsider was lost for evars subject
to restriction (field last_mods was not updated and conversion
problems not considered to be changed).
|
|
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).
|
|
|
|
|
|
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
|
|
|
