| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
notations in R)
Reviewed-by: erikmd
Reviewed-by: ppedrot
|
|
'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
|
|
Reviewed-by: MSoegtropIMC
|
|
The `Print Canonical Projections` command now can take constants and prints only
the unification rules that involves or are synthesized from given constants.
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
* This patch is a quick fix that removes part of the features of coq/coq#10022,
namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged
relation R. This just means we'll need to do an extra step [rewrite UnderE.]
which was unnecessary with Coq 8.11+alpha.
* This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient
feature of coq/coq#10022 (generalize under & over to any Reflexive relation).
* Related: coq-community/atbr#23
|
|
This should have been running already, but it was forgotten in #9872
|
|
Changes to the test-suite were backported from PR #11288.
|
|
|
|
|
|
Might be improvable further. In the first example, we have two
environments involved and one is implicit. It does not seem excluded
that a variable name of the second environment shows up which is not
listed in the first environment.
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
This highlights the fact that diamond inheritance of a custom entry
is a tricky problem, as well as merely importing two custom entries with
the same name from two different modules. The only sane way to give a
semantics to that is to stick to module-scoped objects, i.e. give those
entries a kernel name. In the meantime, I went for a warning when
overriding entries.
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: gares
|
