| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
with #7142]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Closes #6782
|
|
In the META file, the set of base libraries is determined by the
dependencies of the `coq.clib` package.
We add `num` to the dependencies as otherwise dynamically loading
`micromega` and `nsatz` will fail as they require the toplevel to have
`num` linked in.
|
|
This fixes #5675 (in yet another way).
The issue was that `$` (end of string regex) was not properly escaped in
`"`s.
This handles the issue that is displayed in
```
cat A.v.timing.diff
After | Code | Before || Change | % Change
---------------------------------------------------------------------------------------------------
0m01.44s | Total | 0m01.56s || -0m00.12s | -7.92%
---------------------------------------------------------------------------------------------------
0m00.609s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.627s || -0m00.01s | -2.87%
0m00.527s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.552s || -0m00.02s | -4.52%
0m00.304s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.379s || -0m00.07s | -19.78%
N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.006s || -0m00.00s | -100.00%
0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A
--- A.v.timing.diff.desired.processed 2018-03-23 22:22:19.000000000 +0000
+++ A.v.timing.diff.processed 2018-03-23 22:22:19.000000000 +0000
@@ -1,4 +1,4 @@
- N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | N/A
+ N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | -%
------
------
After | Code | Before || Change | % Change
```
where, because `Declare Reduction` takes 0.006s rather than 0s, the %
change shows up as -100% rather than N/A.
|
|
|
|
|
|
Recent commits introduced global flags, but these should be
module-specific so relocating.
Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced
to the truly global stuff.
|
|
We solve some modularity and type duplication problems by moving types
to a better place. In particular:
- We move tactics types from `Misctypes` to `Tactics` as this is their
proper module an single user [with LTAC].
- We deprecate aliases in `Tacexpr` to such tactic types.
cc: #6512
|
|
Minor, a couple of tactic-related types moved.
|
|
tclTHENFIRST/tclTHENLAST, informative version of shelve unifiable
|
|
|
|
|
|
Scope
|
|
When interrupting goal printing, we should continue the loop with the
newly generated state, that should help avoiding synchronization
problems as in #7142.
Fixes #7142.
|
|
We remove meta-information from the query classification and we don't
process `Stm.query` as a transaction anymore, as the right API is
available to it to execute the command directly.
This simplifies pure commands and removes some impossible cases.
Depends on #7138.
|
|
This command is legacy, equivalent to `EditAt` and only used by
Emacs. We move it to the toplevel so we can kill some legacy code and
in particular the `part_of_script` hack.
|
|
We forbid calling `EConstr.to_constr` on terms that are not evar-free,
as to progress towards enforcing the invariant that `Constr.t` is
evar-free. [c.f. #6308]
Due to compatibility constraints we provide an optional parameter to
`to_constr`, `abort` which can be used to overcome this restriction
until we fix all parts of the code.
Now, grepping for `~abort:false` should return the questionable
parts of the system.
Not a lot of places had to be fixed, some comments:
- problems with the interface due to `Evd/Constr` [`Evd.define` being
the prime example] do seem real!
- inductives also look bad with regards to `Constr/EConstr`.
- code in plugins needs work.
A notable user of this "feature" is `Obligations/Program` that seem to
like to generate kernel-level entries with free evars, then to scan
them and workaround this problem by generating constants.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
statement".
|
|
|
|
This has come up a couple times.
|
|
|
|
Thanks to Calvin Beck for porting this chapter.
|
|
|
|
Thanks to Laurent Théry for porting this chapter.
|
|
|
|
Constrextern.explicitize expected that if implicits were declared they
would be declared at least up to the principal argument of the
projection, but Context/discharge of implicits does not preserve this.
Note the anomaly only happens with primitive projections DISABLED in
recent Coqs (>=8.8).
Implicit argument experts may consider whether ensuring enough
implicits are declared would be better.
|
|
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.
|
|
[skip ci]
|
|
|
