| 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).
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |/ / /
|/| | |
| | | |
| | | | |
Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug.
|
| | |/ /
|/| |
| | |
| | | |
This fixes Théo's bug on eset.
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
printing only
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| |\ \ \ \ \ \
| |_|_|/ / /
|/| | | | | |
|
| | |/ / / /
|/| | | |
| | | | | |
This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | | |
This fixes the discrepancy between "rewrite H with (1 := x)"
and "setoid_rewrite H with (1 := x)".
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | |/ / / /
|/| | | | |
|
| | | | | | |
|
| |/ / / / |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | | |
|
| |\ \ \ \ \
| |/ / / /
|/| | | | |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| |/ / / |
|
| |\ \ \
| | | |
| | | |
| | | | |
"Print Assumptions".
|
| |\ \ \ \ |
|
| | | | | | |
|
| |\ \ \ \ \ |
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | | |
We assume Coq always outputs UTF-8 (is it really the case?) and cut strings
after 30 UTF-8 characters instead of using the standard String function.
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| |/ / / / |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
with evars).
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| | |_|_|/ / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
This development of @bmsherman tests universe polymorphism and setoid
rewriting in type, and should build with v8.6 and trunk.
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
- 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).
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
reason I overlooked the result, maybe a missing make clean.
As for testing on the travis test architecture, I could have done
it. This is a question of compromise. I was so certain that it would
work that I did not test. And anyway, the travis test is not absolute
either.
In any case, I'm very sorry about the confusion it introduced.
~~~~ BY THE WAY, NO NEED TO SHOUT ~~~~
~~~~ IT IS A BIG MISCONCEPTION ABOUT HUMAN BEINGS ~~~~
~~~~ TO BELIEVE THAT THEY DO MISTAKES INTENTIONALLY ~~~~
Thank you!
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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!
|
Jason Gross
Maxime Dénès
Théo Zimmermann
Pierre Letouzey
Amin Timany
Hugo Herbelin
Paul Steckler
Jason Gross
Cyprien Mangin
Pierre-Marie Pédrot