| Age | Commit message (Collapse) | Author |
|---|
|
|
|
tclTHENFIRST/tclTHENLAST, informative version of shelve unifiable
|
|
|
|
|
|
Scope
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
statement".
|
|
|
|
This has come up a couple times.
|
|
|
|
When `build` was made to build the doc it dropped `-coqide opt` and
dropped the environment variables for building coqide.
The combination means that when the cache had lablgtk in
opam (installed by some other job) configure would pick it up but the
system package wouldn't be there causing a failure. When lablgtk isn't
in the cache everything was fine.
|
|
|
|
We use a lower level function that accesses the proof without raising an
anomaly. This is a direct candidate for backport, so I used a V82 API but
eventually this API should be cleaned up.
|
|
|
|
|
|
Like CHANGES, and the test-suite folder, this file receives too many
updates to have a code owner. It is the job of the reviewer of the PR
to review changes to these files as well.
|
|
This is done by not failing for fix/cofix while translating from
glob_constr to constr_pattern.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Design choice: Failing with an anomaly or with a catchable Ltac error
"Fail": we fail with a Fail as it was the case with the related
constrained version of tclTHENFIRST/tclTHENLAST.
|
|
|
|
|
|
|
|
|
|
|
|
AppVeyor fail.
|
|
|
|
|
|
|
|
|
|
For instance, error in "Goal forall a f, f a = 0" is now located.
|
|
- The case 0 makes the code of intros until (and in particular of
Detyping.lookup_quantified_hypothesis_as_displayed more complicated).
- The introduction pattern "*" is compositional while "until 0" is not.
|
|
|
|
|
|
|
|
The script now performs many more checks and reports errors in
a more intelligible way.
|
|
|
