| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
Broke the build.
This reverts commit ef6459b00999a29183edc09de9035795ff7912e9.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
We passed the arc to be marked as visited to the functions pushing the
neighbours on the remaining stack, but this can be actually done before
pushing them, as the [process_le] and [process_lt] functions do not rely
on the visited flag. This exposes more clearly the invariants of the
algorithm.
|
| |
|
|
|
|
|
| |
A possible script breakage can occur if one has a notation
at level 11 that is also right associative (now 11 is left associative).
Thanks Georges for debugging that.
|
| |
|
|
|
|
| |
Since commit 2f521670fbd, the Require "file" syntax was not used anymore by
coqtop but the code handling it was still there in coqdep. We finish the work
by erasing the remnant code.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
| |
|
|
| |
Tracing with gdb by Alec Faithfull
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
In case we need to backtrack on universe inconsistencies when converting
two (incompatible) instances of the same constant and unfold them.
Bug reported by Amin Timany.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
|
| |
|
|
|
| |
- Proper [family] implementation
- Use the tailor made hash function for Sorts.t in two places.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
There are still two items I do not undertand fully (the last one about
-extra-phony, and the removal of external libraries at make clean time,
that I could not reproduce on a toy example.
|
| | |
|
| | |
|
Maxime Dénès
Matthieu Sozeau
mlasson
Pierre-Marie Pédrot
Guillaume Melquiond
Hugo Herbelin
Enrico Tassi
Lionel Rieg
Assia Mahboubi