| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: mattam82
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: kyoDralliam
|
|
Reviewed-by: ppedrot
|
|
indirectly dependent in goal
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
|
|
This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18.
We instead add a warning in the manual and a kludge in the test-suite.
|
|
Copy tclWRAPFINALLY to tactics.ml
As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and
https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't export
it from Proofview, because it seems somehow not primitive enough. But
we don't export it from Tactics because it is more of a tactical than a
tactic. But we don't export it from Tacticals because all of the
non-New tacticals there operate on `tactic`, not `Proofview.tactic`, and
all of the `New` tacticals that deal with multi-success things are
focussing, i.e., apply their arguments on each goal separately (and it
even says so in the comment on `New`), whereas it's important that
`tclWRAPFINALLY` doesn't introduce extra focussing.
|
|
As per https://github.com/coq/coq/pull/12129#issuecomment-619389803
Note that we need to work around #12179 in doc of with_strategy
|
|
|
|
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.
We have some timeouts in the strategy success file. We should not run
into issues, because we are not really testing how long these take. We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.
Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.
One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556
Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
|
|
multiple scopes for the same inductive)
|
|
Reviewed-by: pi8027
Reviewed-by: zeldovich
|
|
Part of the plan of #11840.
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
This is saner behavior making subst reversible, as discussed in #12139.
This also fixes #10812 and #12139.
In passing, we also simplify a bit the code of "subst_all".
|
|
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`.
Fixes #12257
Fixes #12258
|
|
Reviewed-by: gares
|
|
|
|
same inductive)
Numeral Notations now play better with multiple scopes for the same
inductive. Previously, when multiple numeral notations where defined
for the same inductive, only the last one was considered for
printing. Now, we proceed as follows
1. keep only uninterpreters that produce an output (first
List.map_filter)
2. keep only uninterpretation for scopes that either have a scope
delimiter or are open (second List.map_filter)
3. the final selection is made according to the order of open scopes,
(find_uninterpretation) or or according to the last defined
notation if no appropriate scope is open (head of list at the end)
|
|
Fixes #12196
|
|
|
|
Reviewed-by: MSoegtropIMC
|
|
Force Cauchy modulus equal to identity, make division transparent
Fix test
|
|
Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat.
The required declarations are now added in ZifyInst.
|
|
Reviewed-by: ejgallego
|
|
in record tuples
Reviewed-by: ejgallego
|
|
Instead, we register functions dynamically declaring the dependencies of the
scheme to be generated.
We had to fix the test-suite because an internal scheme name changed.
We could also tweak the internal flag of scheme dependencies, but in this
particular case it looks more like a bug from the previous implementation.
|
|
Reviewed-by: ejgallego
Reviewed-by: jfehrle
|
|
Reviewed-by: anton-trunov
Reviewed-by: ppedrot
|
|
Reviewed-by: MSoegtropIMC
|
|
Convert into a performance test
Put time bound at the beginning of file
Add Time command in the test
|
|
|
|
The Python scripts now support `--no-include-mem` to turn it off, and
also support `--sort-by-mem`.
Closes #11575
|
|
Closes #5445
Note that we use `Include` rather than `Export` to expose the machinery
defined in `NsatzTactic` from `Nsatz` to preserve backwards
compatibility with developments relying on absolute names of the
constants previously defined in `Nsatz.v`.
|
|
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ppedrot
|
|
entries with a global rule
Reviewed-by: ejgallego
Ack-by: gares
|
|
|
|
constructor.
Moreover, the link to the constructor was hiding other contents of the
tuple.
|
|
Reviewed-by: SkySkimmer
|
|
custom induction scheme
Reviewed-by: ppedrot
|
