| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: MSoegtropIMC
|
|
|
|
|
|
Since we don't always have the call trace anymore, we explicitly
insert a catch of failures in TacAlias. The trace is then treated in
this catch rather than propagated to the underlying calls (a VFun?). I
hope this is doing the same.
The suggestion to use a tclOR is from P.-M. Pédrot.
Note: this is not fully ideal, the messages which were expecting a
trace should be rethought to take into account either that the calls
are not printed anymore, or to print them again.
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
|
|
|
|
This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18.
We instead add a warning in the manual and a kludge in the test-suite.
|
|
We need to record the transparency information in the libobject stack in
order for coqchk to not trip over the strategy information.
This is quite sketchy, though.
|
|
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.
|
|
|
|
This is the bug
https://github.com/coq/coq/pull/12129#issuecomment-619613779
|
|
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>
|
|
|
|
|
|
|
|
|
|
We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?
This is unfortunately a rather large commit. I suggest reading it in
the following order:
* test-suite/output/ZSyntax.{v,out} new test
* test-suite/output/Int63Syntax.{v,out} ''
* test-suite/output/QArithSyntax.{v,out} ''
* test-suite/output/RealSyntax.{v,out} ''
* test-suite/output/FloatSyntax.{v,out} ''
* interp/numTok.ml{i,} extending numeral tokens
* theories/Init/Hexadecimal.v adaptation of Decimal.v
for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v new interface for Numeral Notation (basically,
a numeral is either a decimal or an hexadecimal)
* theories/Init/Nat.v add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v '' positive
* theories/ZArith/BinIntDef.v '' Z
* theories/NArith/BinNatDef.v '' N
* theories/QArith/QArith_base.v '' Q
* interp/notation.ml{i,} adapting implementation of numeral notations
* plugins/syntax/numeral.ml ''
* plugins/syntax/r_syntax.ml adapt parser for real numbers
* plugins/syntax/float_syntax.ml adapt parser for primitive floats
* theories/Init/Prelude.v register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
had to be permuted)
|
|
"decimal" would no longer be an appropriate name when extending to
hexadecimal for instance.
|
|
|
|
Fill in the proofs, adding a few neessary lemmas along the way.
|
|
|
|
|
|
It was removed by #11703.
|
|
Add real numbers up to 10
|
|
|
|
|
|
multiple scopes for the same inductive)
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
|
|
Reviewed-by: pi8027
Reviewed-by: zeldovich
|
|
|
|
|
|
Part of the plan of #11840.
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
|
|
The API in `DeclareDef` should become the recommended API in `Declare`.
This greatly reduces the exposure of internals; we still have a large
offender in `Lemmas` but that will be taken care of in the next
commit; effectively removing quite some chunks from `declare.mli`.
This PR originally introduced a dependency cycle due to:
- `Declare`: uses `Vernacexpr.decl_notation list`
- `Vernacexpr`: uses `ComHint.hint_expr`
- `ComHint`: uses `Declare.declare_constant`
This is a real cycle in the sense that `ComHint` would have also move
to `DeclareDef` in the medium term.
There were quite a few ways to solve it, we have chosen to
move the hints ast to `Vernacexpr` as it is not very invasive
and seems consistent with the current style.
Alternatives, which could be considered at a later stage are for
example moving the notations AST to `Metasyntax`, having `Declare` not
to depend on `Vernacexpr` [which seems actually a good thing to do in
the medium term], reworking notation support more deeply...
|
