| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
case of missing record field
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
As stated in the manual, the fourier tactic is subsumed by lra.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.
This is used to provide better error messages on missing record
fields.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
For now we only copy the templates, but we could do more fancy stuff.
This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We make it possible to deprecate tactics defined by `Ltac`, `Tactic
Notation` or ML.
For the first two variants, we anticipate the syntax of attributes:
`#[deprecated(since = "XX", note = "YY")]`
In ML, the syntax is:
```
let reflexivity_depr =
let open CWarnings in
{ since = "8.5"; note = "Use admit instead." }
TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr
[ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
END
```
A warning is shown at the point where the tactic is used (either
a direct call or when defining another tactic):
Tactic `foo` is deprecated since XX. YY
YY is typically meant to be "Use bar instead.".
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | |/
|/| |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
|
| |/ / |
|
| |\ \
| | |
| | |
| | | |
format).
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In some cases, Format's inner boxes inside an outer box act as break
hints, even though there are already "better" break hints in the outer
box.
We work around this "feature" by not inserting a box around the
default printing rule for a notation if there is no effective break
points in the box.
See https://caml.inria.fr/mantis/view.php?id=7804 for the related
OCaml discussion.
|
| |/ / |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We fix the issue by removing terms of the substitutions which have
free variables and are thus not interpretable in the context of the
"ltac:" subterm.
This remains rather ad hoc, since, in an expression "Notation f x :=
ltac:(foo)", we interpret "x" at calling time of "foo" rather than at
use time of "x" in foo, even if "x" is not necessary.
We could also imagine that binders in the ltac expressions are then
interpreted but that would start to be (very) complicated.
Note that this will presumably "fix" ltac2 quotations at the same
time.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
subtyping.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | |_|_|/ / /
|/| | | | | |
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
When launched through PATH argv.(0) is just the command name.
eg "coqtop -compile foo.v" -> argv.(0) = "coqtop"
Using executable_name also follows symlinks but this isn't tested to
avoid messing with windows. Running Coq through a symlink is not as
important as PATH anyways.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
When inferring [u <= v+k] I replaced the exception and instead add
[u <= v]. This is trivially sound and it doesn't seem possible to have
the one without the other (except specially for [Set <= v+k] which was
already handled).
I don't know an example where this used to fail and now succeeds (the
point was to remove an anomaly, but the example
~~~
Module Type SG. Definition DG := Type. End SG.
Module MG : SG. Definition DG := Type : Type. Fail End MG.
~~~
now fails with universe inconsistency.
Fix #7695 (soundness bug!).
|
| | | |_|/ / /
| |/| | | | |
|
| |/ / / / / |
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | | |
It seems that lifting a term with a negative index is not equivalent to
strengthening it by applying to a dummy substitution. This looks suspicious
at best.
|
| |/ / / |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | | |
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
| |\ \ \
| | | |
| | | |
| | | | |
to "match").
|
| |\ \ \ \ |
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | | |
This ensures that computations are shared as much as possible, mimicking
the "positive" records computational behavior if possible.
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | |
| | | |
Although the fix is not a proper one, it seems to solve
every instance of #2800 that could be tested.
|
| |\ \ \
| | | |
| | | |
| | | | |
of submodules.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
to anomaly)
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
in unification
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We had mostly used absolute links in the past.
I just discovered that GitHub recommends using relative links instead:
https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links
and indeed my Emacs Markdown mode can handle relative links but doesn't
interpret absolute links relatively to the root of the git repository.
[ci skip]
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This is a quick fix. Code should be made nicer along these lines:
- try to pass the name of the variable created by "mkletin_goal" in
the monad using "refine_one";
- use a disjunctive type of "inhyps" to indicate when it is
meaningful, rather than using [].
|
| | |/ / / / /
|/| | | | | |
|
Pierre-Marie Pédrot
Enrico Tassi
Maxime Dénès
Siddharth Bhat
Emilio Jesus Gallego Arias
Matthieu Sozeau
Gaëtan Gilbert
Jasper Hugunin
Vincent Laporte
Matthieu Sozeau
Hugo Herbelin
Cyprien Mangin
Théo Zimmermann