| Age | Commit message (Collapse) | Author |
|---|
|
decidability scheme).
Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:
Set Decidable Equality Schemes.
Inductive a := A with b := B.
which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
|
|
|
|
"Print Module command shows module type expression incorrectly".
|
|
The .png was ugly (less than 400px wide) and did not match the content of
the .fig file (e.g. presence of '$'). To improve things a bit, text is now
rendered by latex.
|
|
|
|
The quadratic behaviour of list searching probably appears with small
enough samples. With the advent of usable libraries in Coq, and thus many
possible dependencies, better be safe than sorry.
|
|
|
|
On Fedora, `which 2>&1 >/dev/null` doesn't silence stderr, while `which >/dev/null 2>&1` does.
|
|
|
|
|
|
The file seems to have been reintroduced by error by commit 012fe1a96, but
it was not compiled anyway.
|
|
|
|
|
|
Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
|
|
I was not seeing the warning due to the 10 deprecation warnings before
it...
|
|
|
|
|
|
unification in tactics.
The relaxing of occur-check was ok but was leading trivial problems of
the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into
?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems
was not any more able to deal with.
Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way,
so that it behaves as if the occur-check had not been restricted.
|
|
using closer naming strategies for naming variables in make_all_name_different
and when contracting trivial letins.
Not sure what the best policy is. Maybe the contraction process should
not invent names at al and let make_all_name_different do the job.
Maybe pretyping should name all rels which it pushes to environment
(with cases.ml paying attention to avoid clash).
The problem shows for instance with a PretypeError (... env, ... ,
ActualTypeNotCoercible (NotClean (... env ...)) message with two
copies of env which we don't if they are the same but which have to
share same names for similar rendering of the rels!
This was revealed e.g. by the error message of #4177.
|
|
This is a bug in a pretty old code, showing also in 8.3 and 8.4.
|
|
|
|
former filter after 48509b61 and 3cd718c, because filtered let-ins
were not any longer preserved).
|
|
|
|
Patch by Matthieu Sozeau.
Fixes #3819: "Error: Unsatisfied constraints" due to canonical
structure inference
|
|
We were throwing away constraints from 'with Definition' in module
type ascriptions.
|
|
because of the name of a bound variable lost when unifying under a
binder in evarconv.
|
|
Indeed, the name of a bound variable was lost when unifying under a Prod in
evarconv.
The error message for "Unable to satisfy the following constraints" is
still to be improved though.
|
|
I was trying to be a bit too clever with not substituting the universe
instance everywhere: the constructor type/inductive arity has to be
instantiated before instantiate_params runs, which became true only
for constructor types since my last commit.
|
|
It showed up at the CoqCS.
|
|
Calling md5sum test earlier, at the time coqchk is built, rather than
at testing time, hopefully moving it closer to what it is supposed to
occur.
|
|
|
|
|
|
|
|
Commit df6e64fd28 let apply_coercion raise NoCoercion untrapped by inh_app_fun.
Commit 4944b5e72 caught NoCoercion but missed re-attempting inserting a
coercion after resolving instances of type classes.
This fixes MathClasses (while preserving fix of part of from 4944b5e72
and fixes of HoTT_coq_014.v from df6e64fd28).
|
|
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
|
|
|
|
|
|
|
|
Fixes #4139 (Not_found exception with Require in modules).
|
|
Avoid undeeded large substitutions, and add test-suite file for
fixed bug 4283 in closed/
|
|
Fixes bug #4176 (actually two bugs in one)
Correct computation of the type of primitive projections in presence of
let-ins.
|
|
Since Guillaume's, launching coqtop without -native-compiler and call
native_compute would mean recompiling silently all dependencies, even if they
had been precompiled (e.g. the stdlib).
The new semantics is that -native-compiler disables separate compilation of the
current library, but still tries to load precompiled dependencies. If loading
fails when the flag is on, coqtop stays silent.
|
|
Reviewed by M. Sozeau
This commit fixes template polymorphism and makes it more precise,
applying to non-linear uses of the same universe in parameters of
template-polymorphic inductives. See bug report and
https://github.com/coq/coq/pull/69 for full details.
I also removed some deadcode in checker/inductive.ml.
I do not know if it is also necessary to fix checker/indtypes.ml.
|
|
Unfortunately, it seems that retyping can be called in ill-typed terms and/or in
the wrong environment. This was broken for projections by my commit
a51cce369b9c634a93120092d4c7685a242d55b1
|
|
They do not have eta-rule indeed, even though it was displayed as such.
|
|
Correct folding order over the named_list_context.
|
|
|
|
Wrong handling of mind_params_ctxt...
|
|
|
|
|
