| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
Commit dc438047 was a bit overlooked as it introduced a wrong comparison function
on term patterns in dnets. Strangely enough, it seems not to have wreaked havoc
that much compared to the severity of the error.
|
| |
|
|
|
|
|
|
| |
File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.
There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
|
| | |
|
| |
|
|
|
|
|
| |
abbreviation not bound to an applied constructor as itself but rather
as a binding variable as it was the case for non-applied
constructor). This was broken by e5c02503 while fixed #3483 (Not_found
uncaught with a notation to a non-constructor).
|
| | |
|
| |
|
|
|
| |
This should actually probably be an anomaly, but I'm unsure the code
for decidability schemes is robust enough to dare it.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
Pierre-Marie Pédrot
Guillaume Melquiond
Hugo Herbelin
Jason Gross
Gregory Malecha
Matthieu Sozeau
Maxime Dénès
Matthieu Sozeau
Enrico Tassi
mlasson