| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
with binders)
|
| |\ \ |
|
| | |/
|/| |
|
| |\ \
| | |
| | |
| | | |
masked).
|
| | |/
|/|
| |
| |
| |
| |
| | |
- https://coq.inria.fr/bugs/show_bug.cgi?id=5529
- https://coq.inria.fr/bugs/show_bug.cgi?id=5537
See also PR #640
|
| | |
| |
| |
| |
| |
| |
| | |
Was working when calling test-suite from main Makefile but not when
calling directly from the test-suite Makefile.
The dependency was mistakenly dropped in 98a927aef.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.
We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.
Of course, the question of what best unification error to give in the
presence of backtracking is still open.
|
| |\ \
| |/
|/|
| | |
tricks available to users
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |_|_|/
|/| | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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"
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The rule is that any file misc/*.sh will now be automatically executed
from the test-file directory with appropriate environment variables
set. The test can use any auxiliary material which is put in a
directory of the same name as the test.
This avoids making the main Makefile more or more complex.
We loose some customization though (no more custom messages such as
printing of the number of universes in the test about the number of
necessary universes). We could preserve such customization if needed
but I did not consider it was worth the effort.
Warning: specific targets universes, deps-order, deps-checksum are
removed by consistency. Do instead "make misc/universes.log", etc., or
even "make misc" for all.
|
| | | | | | | | |
|
| | | | | | | | |
|
| | |_|_|/ / /
|/| | | | | |
|
| |\ \ \ \ \ \ |
|
| | |_|_|/ / /
|/| | | | | |
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| |\ \ \ \ \ \ \
| |_|_|_|_|_|/
|/| | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The addition to the test suite showcases the usage.
|
| |\ \ \ \ \ \ \
| |_|/ / / / /
|/| | | | | | |
|
| | | | | | | |\
| | | | | | | |
| | | | | | | |
| | | | | | | | |
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).
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
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...
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
let-ins
|
| | | | | | | | |
|
| | |_|_|_|/ /
|/| | | | |
| | | | | |
| | | | | | |
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.
|
| | |/ / / / / /
|/| | | | | | |
|
| | | |/ / / /
| |/| | | | |
|
Maxime Dénès
Hugo Herbelin
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Pierre Courtieu
Cyprien Mangin
Gaetan Gilbert
Paul Steckler
Jason Gross