| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
| |
The issue was due to the fact that unfold hints are given a priority of 4
by default. As eauto was now using hint priority rather than the number of
goals produced to order the application of hints, unfold were almost always
used too late. We fixed this by manually giving them a priority of 1 in the
eauto tactic.
Also fixed the relative order of proof depth w.r.t. hint priority. It should not
be observable except for breadth-first search, which is seldom used.
|
| |
|
|
|
| |
definition, if they manipulate structures depending on the initial state
of the context.
|
| |
|
|
|
| |
constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- Introduced an error: fold was counting in the wrong direction and I
did not test it. Sorry.
- Substitution from params-with-let to params-without-let was still
not correct.
Hopefully everything ok now. Eventually, we should use canonical
combinators for that: extended_rel_context to built the instance and
and a combinator apparently yet to define for building a substitution
contracting the let-ins.
|
| |
|
|
| |
pattern-matching on function calls.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
projections.
- lift accounting for the record missing in computing the subst from
fields to projections of the record
- substitution for parameters should not lift the local definitions
- typo in building the latter (subst -> letsubst)
|
| |
|
|
|
| |
Everywhere we know that the universes of the left argument are an
extension of the right argument, we do not have to merge universes.
|
| |
|
|
|
|
| |
The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
|
| |
|
|
| |
about the prehistory of Coq.
|
| | |
|
| | |
|
| |
|
|
|
| |
We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.
|
| | |
|
| |
|
|
| |
Mention compatibility file.
|
| | |
|
| | |
|
Hugo Herbelin
Matthieu Sozeau
Enrico Tassi
Pierre-Marie Pédrot
Matthieu Sozeau
Guillaume Melquiond
Maxime Dénès
Jason Gross