| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | |/
|/| |
|
| |\ \
| |/
|/| |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019),
"[zify] loops on dependent types"; before, we would see a `Z.of_nat (S
?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a
hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a
hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on
this.
This may not be the "right" fix (there may be cases where `zify` should
succeed where it still fails with this change), but this is a pure
bugfix in the sense that the only places where it changes the behavior
of `zify` are the places where, previously, `zify` looped forever.
|
| | | | |
|
| |\ \ \
| |_|/
|/| | |
|
| |\ \ \
| | | |
| | | |
| | | | |
(EDIT: for mutual fixpoints)
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
section variables.
|
| | |_|/ /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Two issues in one:
- some focused_simpl were called on the wrong locations
- some focused_simpl were done on whole equations
In the two cases, this could be bad if "simpl" goes too far
with respect to what omega expects: later calls to "occurrence"
might fail. This may happen for instance if an atom isn't a variable,
but a let-in (b:=5:Z in the example).
|
| |\ \ \ \ |
|
| | |/ / /
|/| | |
| | | |
| | | | |
This fixes Théo's bug on eset.
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
printing only
|
| | |/ / / /
|/| | | | |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| |/ / / / / |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| |/ / / / |
|
| | |_|/
|/| | |
|
| | | | |
|
| |\ \ \
| | | |
| | | |
| | | | |
with evars).
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | | |
The cause was a missing evar/evar clause in ltac pattern-matching
function (constr_matching.ml).
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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...
|
| | | | |
|
| | | | |
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | | |
Add a test-suite file to be sure we won't regress silently.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
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...
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This allows e.g. to use the record notations even when there are
defined fields.
A priori fixed also missing parameters when interpreting primitive
tokens.
|
| | |/
|/| |
|
| |\ \
| | |
| | |
| | | |
Was needed to be done for a while.
|
| | | | |
|
| | | | |
|
| | |/
|/| |
|
Maxime Dénès
Paul Steckler
Théo Zimmermann
Jason Gross
Pierre Letouzey
Hugo Herbelin
Pierre-Marie Pédrot
Cyprien Mangin
Gaetan Gilbert
Matthieu Sozeau
Julien Forest
Julien Forest