| Commit message (Collapse) | Author | Age |
|\
| |
| |
| |
| | |
Was PR#389: Changed mention of deprecated -byte option to .byte suffix;
change module for Coq loop
|
| | |
|
|/ |
|
|
|
|
|
|
|
|
|
|
|
| |
Some C files included in build scripts (in dev/build) were triggering
errors or warnings on non-win32 platforms.
Note that ide/ide_win32_stubs.c was already handled through an ad-hoc
rule in Makefile.
If you add a new C file outside of kernel/byterun, please extend the CFILES
variable.
|
|\
| |
| |
| | |
Was PR#366: Univs: fix bug 5208
|
|\ \
| | |
| | |
| | | |
Was PR#378: Univs: fix bug #5188
|
| | | |
|
| | | |
|
|\ \ \
| | | |
| | | |
| | | | |
Was PR#377: Univs: fix bug #5180
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#368: Add example in dev/doc/changes involving Tacmach.project
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Parts of PR#367: Fixing the "beautifier" and checking the
parsing-printing reversibility
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Was a bug introduced in 0ad6edc1.
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
became mandatory.
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Parameter was implemented the wrong way trying to separate the universes
of the telescope.
|
|\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Was PR#381: V8.6+fix typeclasses eauto shelving
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
We make this warning configurable and disabled by default.
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
with user-level notations by inserting spaces.
|
| |/ / / / / /
|/| | | | | | |
|
|\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Was PR#380: Fix bug #5232: proper globalization of hints paths
|
|\ \ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Was PR#369: Make a note about wit_constr and Constrarg in
dev/doc/changes
|
|\ \ \ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Was PR#371: Update dev/doc/changes with things about mem_named_context
|
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Was PR#364: Add missing label. Fixes broken ref.
|
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Was PR#382: [merlin] Adjust merlin for ide.
|
|/ / / / / / / / / / / |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Before this fix, unshelve typeclasses eauto would produce sub-goals
in the reverse order compared to when they were first shelved.
|
| |_|_|_|/ / / / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
A file in the test-suite had to be modified.
It was supposed to reproduce a behavior in intuistionistic-nuprl
but it did not really.
This commit is not supposed to break intuistionistic-nuprl.
|
| |_|_|/ / / / / /
|/| | | | | | | | |
|
| | | | | | |/ /
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
In the kernel's generic conversion, backtrack on UniverseInconsistency
for the unfolding heuristic (single backtracking point in reduction).
This exception can be raised in the univ_compare structure to produce
better error messages when the generic conversion function is called
from higher level code in reductionops.ml, which itself is called during
unification in evarconv.ml.
Inside the kernel, the infer and check variants of conversion never
raise UniverseInconsistency though, so this does not change the behavior
of the kernel.
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
| |_|_|_|_|_|/
|/| | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
When opening a file without extension, an uncaught exception was
occurring.
Note that this fix is not complete, since the "Compile Buffer" command
still fails. This is because of a limitation of coqc which appends the
".v" extension to its argument even if it already existed (and even if
it doesn't exist with the extension!).
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We introduce a bit of compatibility parsing code to print deprecation
warnings.
|
| |_|_|_|_|/
|/| | | | |
| | | | | |
| | | | | | |
Line erroneously removed in 17f3346c
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
If the result had its 30th bit set, then all the high part of the result
on a 64-bit architecture would end up being set, thus breaking subsequent
computations.
This patch also fixes the incorrectly parenthesized definition of
uint32_of_value, which by luck was never misused.
|
| | | | | | |
|
| |_|_|_|/
|/| | | | |
|
| |/ / /
|/| | | |
|
| |/ /
|/| | |
|
| |/
|/| |
|