| Age | Commit message (Collapse) | Author |
|---|
|
|
|
notations (+ a fix about locations)
Reviewed-by: ppedrot
|
|
- Add a `--fuzz` option to `make-both-single-timing-files.py`
Passing `--fuzz=N` allows differences in character locations of up to
`N` characters when matching lines in per-line timing diffs.
The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`.
See also the discussion at
https://github.com/coq/coq/pull/11076#pullrequestreview-324791139
- Allow passing `--real` to per-file timing scripts and `--user` to
per-line timing script.
This allows easily comparing real times instead of user ones (or vice
versa).
- Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build
- We also now use argparse rather than a hand-rolled argument parser;
there were getting to be too many combinations of options.
- Fix the ordering of columns in Coq's build system; this is the
equivalent of #8167 for Coq's build system.
Fixes #11301
Supersedes / closes #11022
Supersedes / closes #11230
|
|
+ tests in the test-suite for non max local implicit arguments
|
|
|
|
termination checker.
Reviewed-by: SkySkimmer
|
|
There was an evar leak due to an evarmap not being threaded correctly
when computing open terms.
|
|
Reviewed-by: fajb
|
|
|
|
Fixes #5617.
|
|
- The cutting plane has been (sometimes) improved to generate stronger
cuts.
- There is now some support for profiling the Simplex
see documentation for Show Lia Profile.
|
|
This is probably a bit overkill but users are tempted to experiment
it, so we accept that both ends of a recursive notation are surrounded
with boxes which contain printing hints.
The alternative would have been to forbid the ends of a recursive
notation to be in boxes, but strictly speaking it is a bit more
restricting, even if I don't see a realistic use of the general form.
|
|
This shows a few bugs and even anomalies. See issue #11091.
See further commits for some fixes.
|
|
Reviewed-by: ppedrot
|
|
notations in R)
Reviewed-by: erikmd
Reviewed-by: ppedrot
|
|
Related: https://github.com/coq/coq/pull/8630
|
|
'e' was not displayed when printing decimal notations in R :
Require Import Reals.
Check (1.23e1, 32e+1, 0.1)%R.
was giving
< (123-1%R, 321%R, 1-1%R)
instead of
< (123e-1%R, 32e1%R, 1e-1%R)
This was introduced in #8764 (in Coq 8.10).
|
|
And enable related test.
|
|
so for instance
~~~coq
Set Printing All. Set Printing Universes.
Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
Lemma bla@{u v|u < v} : foo@{u v} -> False.
Proof. induction 1. Qed.
~~~
works.
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
decorations
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
|
|
OCaml's string type
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: herbelin
Ack-by: maximedenes
Reviewed-by: pi8027
|
|
type of h.
Reviewed-by: ppedrot
|
|
(and not just…
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
The type of h is reconstructed to look as much as the initial type of
h as possible.
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
Fixed by 8750682e367d7e78634bf88e667e4c9e7c3613d3 (#9915)
|
|
|
|
Seems to have been fixed since it was reported (perhaps by #11317?)
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
We typecheck arguments like previously, using bidirectionality hints,
but ultimately replace them with user-provided arguments on which we
replay coercion traces.
This is a fix which should be easy to backport, but there are two
directions of future work:
- Coercion traces for `Program` coercions (in these cases, we currently
use the inferred arguments)
- Separate the Coercion API in two phases: inference and application of
coercions. It will make the approach taken here cleaner, and probably
make it easier to interleave typing steps with coercion inference.
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
- Add an instance to ZifyInst to instruct zify that
0 < x -> 0 < y -> 0 < Z.pow x y
- More aggressive interval analysis to bound non-linear monomials.
|
|
use of var
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
The regexp parsing the time needed an update to support the case
"Finished failing translation". Also, not all cases of failures were
reported.
|
|
Reviewed-by: gares
|
|
|
|
Closes #10491
We re-add the header in doc/tools/coqrst/notations/fontsupport.py
which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6
The fontsupport script itself has been kept for reference, however it
is not involved by any build target as of today.
|
|
clauses in pattern matching decompilation algorithm
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
unification error message
Reviewed-by: ppedrot
|
