| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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.
|
|
Modules inserted into the environment were not hashconsed, leading to an
important redundancy, especially in module signatures that are always fully
expanded.
This patch divides by two the size and memory consumption of module-heavy
files by hashconsing modules before putting them in the environment. Note
that this is not a real hashconsing, in the sense that we only hashcons the
inner terms contained in the modules, that are only mapped over. Compilation
time should globally decrease, even though some files definining a lot of
modules may see their compilation time increase.
Some remaining overhead may persist, as for instance module inclusion is not
hashconsed.
|
|
Not sure if this is really what is expected though.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
unification (not necessarily preserved due to the fo approximation rule).
|
|
only one disjoint component of the typeclasses instances to resolve.
|
|
|
|
|
|
their type annotation.
|
|
We just handle unnamed implicits using a dummy name. Note that the implicit
argument logic should still output warnings whenever the user writes implicit
arguments that won't be taken into account, but I'll leave that for another
time.
|
|
default. Interestingly, there is an example where it makes the rest of
the proof less natural.
Goal forall x y:Z, ...
intros [y|p1[|p2|p2]|p1[|p2|p2]].
where case analysis on y is not only in the 2nd and 3rd case, is not
anymore easy to do.
Still, I find the bracketing of intro-patterns a natural property, and
its generalization in all situations a natural expectation for
uniformity. So, what to do? The following is e.g. not as compact and
"one-shot":
intros [|p1|p1]; [intros y|intros [|p2|p2] ..].
|
