| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| | |
It has been deprecated for a while in favor of `Qed`.
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
We do that by using constr_with_bindings rather than
open_constr_with_bindings (+ extra call to typeclasses in
"specialize"). If my understanding is right, the only effect would be
to succeed more in cases where it was failing (in
inh_conv_coerce_to_gen). In particular, "specialize" and
"contradiction" already have a WITHHOLES test for rejecting pending
holes.
Incidentally, this answers enhancement #5153.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We seized this opportunity to factorize the code for interning `pat
with more general pre-existing code.
More precisely: There was already a function to compute the free
variables of a pattern. Commit c6d9d4fb rewrote an approximation of it
and #5222 hits cases non-treated by this function. We remove the
partially-defined redundant code and use instead the existing code
since intern_cases_pattern, already called, was already doing this
computation. (In doing so, we discover a bug in merging names in the
presence of nested "as" clauses, which we fix in previous
commit. Additionally, intern_local_pattern was misleadingly overkill
to simply mean a folding on Id.Set.add and we avoid the detour.
|
| |\ \
| | |
| | |
| | | |
and 8.5/8.6 "refine"
|
| | | | |
|
| |\ \ \ |
|
| | | | |\
| | | | |
| | | | |
| | | | | |
with evars).
|
| | | | |\ \ |
|
| | | | | | | |
|
| | | | | |/
| | | |/|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.
One day, evar kinds will need a little cleaning...
PS: This is a second attempt, completing db28e82 which was missing the
case PEvar in constr_matching.ml. Indeed the attached fix to #5487
alone made #2602 failing, revealing that the real cause for #2602 was
actually not fixed and that if the test for #2602 was working it was
because of #5487 hiding the real problem in #2602.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
A universe substitution was lacking as the normalized evar map was dropped.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The code was assuming that the terms t and u for which {t=u}+{t<>u} is
proved were distinct. We refine an internal "generalize" of "u" so
that it works on the two precise occurrences to abstract, even if
other occurrences of u occur as subterm of t too.
We also reuse the global constants found in the statement rather than
reconstructing them (this seems better in case the global constants
eventually get polymorphic universes?).
|
| | | |/
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
One day I'll get bored of spending my nights fixing commits that were
pushed without being tested, and I'll ask for removal of push rights.
But for now let's pretend I haven't insisted enough:
~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~
Thank you!
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.
One day, evar kinds will need a little cleaning...
|
| | | | |
|
| |/ /
| |
| |
| | |
pattern-matching for refine.
|
| |\| |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | |
| | | |
| | | | |
Note: I removed what seemed to be dead code in recdef.ml (local_assum
and local_def introduced with econstr branch), assuming that this is
what should be done.
|
| | | |/
| |/| |
|
| | |/
|/| |
|
| | |\ |
|
| | | |
| | |
| | |
| | | |
The bug has been solved as a side-effect of the EConstr branch.
|
| |\| | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We use heaps instead of continuously adding elements to an ordered list,
which was quadratic in the worst case.
As a byproduct, this solves bug #5359, which was due to a stack overflow on
big lists.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
This was assuming dependencies occurring in configurations of
the form x:A, y:B x, z:C x y |- match x, y, z with ... end".
But still work to do for better management of dependencies in general...
|
| |\ \ \ |
|
| | | | | |
|
| | | |/ |
|
| |\ \ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | |
| | | |
Bug #4957 was "unify cannot directly unify universes with evars, but can
do so indirectly".
|
| |\| | |
|
| | |\ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
|
| |\| | | |
|
| | |/ /
| | |
| | |
| | |
| | |
| | | |
Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372)
"Anomaly: Not a valid information when defining mutual fixpoints that
are not mutual with Function".
|
| |\| | |
|
| | |\ \
| | | |
| | | |
| | | | |
correctly as…
|
| | |_|/
|/| |
| | |
| | |
| | | |
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
| |\ \ \
| | | |
| | | |
| | | | |
Tactic Notation
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | | |
In particular, this closes bug 2417.
|
| |\| | |
|
| | |\ \ |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Pierre-Marie Pédrot
Cyprien Mangin
Paul Steckler
Julien Forest
Tej Chajed
Enrico Tassi
Théo Zimmermann