| Age | Commit message (Collapse) | Author |
|---|
|
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]
|
|
|
|
|
|
Thanks to Paul Steckler for porting this chapter.
|
|
|
|
|
|
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.
|
|
Thanks to Matthieu Sozeau for porting this chapter.
|
|
|
|
Thanks to Pierre Letouzey for porting this chapter.
|
|
|
|
|
|
Thanks to Pierre Letouzey for porting this chapter.
|
|
|
|
|
|
|
|
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.
|
|
terms whose branches are in eta-let-expanded canonical form.
This is a hack intended to work only with destruct/case as they are
currently implemented. Would not work with arbitrary proofs of the
form "Cases(ci,p,c,[|...;b;...|] given to logic.ml for which b, if
with Metas, has not the form of an eta-let-expanded Meta.
|
|
This is done by not failing for fix/cofix while translating from
glob_constr to constr_pattern.
|
