| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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...
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adapt to new [projection] abstract type comprising a constant and
a boolean.
|
|
Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
|
|
Using relative path for coqlib, for some reason this fails on Mac OS
X. Took the easiest way to fix it.
|
|
|
|
verbose flag.
|
|
|
|
|
|
|
|
|
|
|
|
I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
|
|
The search algorithm is not satisfactory though, as it crawls through
all known files to find the proper one. We should rather use some trie-based
data structure, but I'll leave this for a future commit.
|
|
Stuck primitive projections were never convertible.
|
|
Triggers a bug in declarative mode. Waiting for someone to volunteer and fix
the bug, but meanwhile I'm trying to fix the test-suite.
|
|
|
|
|
