| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
| |
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
| |\ |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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 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.
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
Although the fix is not a proper one, it seems to solve
every instance of #2800 that could be tested.
|
| |\ \ \
| | | |
| | | |
| | | | |
to anomaly)
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
in unification
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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 [].
|
| |/ / / / |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Redundancy between finding section variables in both interp_var and
interp_qualid could probably be cleaned.
|
| | |_|/
|/| |
| | |
| | | |
Fix #5012.
|
| | |/
|/|
| |
| |
| |
| |
| | |
We store the universe context in the inlined terms and apply it to
the instance provided to the substitution function. Technically the
context is not needed, but we use it to assert that the length of the
instance corresponds, just in case.
|
| |\ \
| | |
| | |
| | | |
vm_compute and native_compute (partial fix to #7068; also fixes #7076))
|
| | | |
| | |
| | |
| | |
| | | |
Dependency analysis for separate compilation was not iterated properly
on rel_context and named_context.
|
| |/ / |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
pattern-matching names
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
tactic unification.
|
| |\ \ \ \ \ \ \ \ |
|
| | |_|_|_|_|_|/ /
|/| | | | | | | |
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
|
| | |_|_|_|/ / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
When creating a scheme for bifinite inductive types, we do not create a
fixpoint.
|
| | | | | | | | | |
|
| | |/ / / / / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The old unification engine was using the unfiltered environment when a
context had been cleared, leading to an ill-typed goal.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Failed in v8.7.2 but were fixed by v8.8.0.
|
| | | | | | | | |
|
| |\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
symlink from repo
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Fixes #7065
|
| | |/ / / / / / |
|
| | | | | | | | |
|
| |/ / / / / / |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
LTAC's `fix` and `cofix` do require access to the proof object inside
the tactic monad when used without a name. This is a bit inconvenient
as we aim to make the handling of the proof object purely functional.
Alternatives have been discussed in #7196, and it seems that
deprecating the nameless forms may have the best cost/benefit ratio,
so opening this PR for discussion.
See also #6171.
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
removing the test.
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We ensure that all original names in a spine of matched nested binders
are distinct.
Note: This enforces that two binders with same internal names are kept
disjoint but this does not enforce that we shall respect names exactly
as they are printed. Only the original prefix of the internal names
are preserved, not their "0" or "1" etc. suffix.
|
| | | | | |/ /
| | | |/| | |
|
Benjamin Barenblat
Matthieu Sozeau
Gaëtan Gilbert
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Cyprien Mangin
Tej Chajed
Théo Zimmermann
Ralf Jung
Emilio Jesus Gallego Arias
Jason Gross