| Age | Commit message (Collapse) | Author |
|---|
|
It was not used in Coq codebase, and the only known user was ssreflect up
to commit 95354e0dee.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
|
|
|
|
|
|
|
|
constraints at the time of Next Obligation/Solve Obligations so that
interleaving definitions and obligation solving commands works properly.
|
|
using the wrong context.
This is very bad style but currently unavoidable, at least we don't
throw an anomaly anymore.
|
|
projections (off by default).
|
|
using dot notation.
|
|
|
|
|
|
longer stable w.r.t. equality constraints as the universe graph will
choose different canonical levels depending on the equalities given to
it (l = r vs r = l).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
|
valid (when Top.i is global and hence > Set).
|
|
|
|
The fix was actually elementary. The lexer comes with a function to
compare parsed tokens against tokens of the parsing rules. It is
enough to have this function considering an ident in a parsing rule to
be equal to the corresponding string parsed as a keyword.
|
|
The nametab in which the error message is printed is not the one in
which the error message happens.
This reveals a weakness in the fix_exn code: the fix_exn function should
be pure, while in some cases (like this one) uses the global state (the
nametab) to print a term in a pretty way (the shortest non-ambiguous name
for constants).
This patch makes the externalization phase (used by term printing)
resilient to an incomplete nametab, so that printing a term in the
wrong nametab does not mask the original error.
|
|
|
|
Instead of accumulating constraints which are not present in the original
graph, we parametrize the equality function by a function actually merging
those constraints in the current graph. This prevents doing the work twice.
|
|
|
|
|
|
second chance to dynamically regenerate the file system cache when a
file is not found (suggested by Guillaume M.).
|
|
correct case on MacOS X whose file system is case-insensitive but
case-preserving (HFS+ configured in case-insensitive mode).
Generalized it to any case-preserving case-insensitive file system,
which makes it applicable to Windows with NTFS used in
case-insensitive mode but also to Linux when mounting a
case-insensitive file system.
Removed the blow-up of the patch, improved the core of the patch by
checking whether the case is correct only for the suffix part of the
file to be found (not for the part which corresponds to the path in
which where to look), and finally used a cache so that the effect of
the patch is not observable.
Note that the cache is implemented in a way not synchronous with
backtracking what implies e.g. that a file compiled in the middle of
an interactive session would not be found until Coq is restarted, even
by backtracking before the corresponding Require.
For history see commits
b712864e9cf499f1298c1aca1ad8a8b17e145079,
4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
69941d4e195650bf59285b897c14d6287defea0f
e7043eec55085f4101bfb126d8829de6f6086c5a.
as well as
https://coq.inria.fr/bugs/show_bug.cgi?id=2554
discussion on coq-club "8.5 and MathClasses" (May 2015)
discussion on coqdev "Coq awfully slow on MacOS X" (Sep 2015)
|
|
When not using ocamlfind, we use a grep-based heuristic to check that lablgtk2
is recent enough. This is an extension of an already-used heuristic.
|
|
This was not a typo (was correctly taking the family type of the type).
|
|
|
|
|
|
non-polymorphic definitions, original universes might be substituted
later on due to constraints.
|
|
|
|
|
|
|
|
|
|
parameters of an inductive type.
|
|
|
|
Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).
Fixing similar error in pretyping.
|
|
instances for each of the inductive in the same block but reuse the
original universe context shared by all of them. Also do not force
schemes to become universe polymorphic.
|
|
contexts.
|
