| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| | |
Previously, the kernel would silently fall back to standard conversion.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
On 64 bits architectures, integers could have some of their 32 msb set to 1
internally in the VM. When read back to a Coq term, this was not observable. But
an equality test would fail. From the user point of view, the symptom was that
vm_compute; reflexivity would succeed but the subsequent Qed would fail.
Bug reported by Tahina Ramananandro.
|
| | |
| |
| |
| | |
ADDMULDIVINT31 was missing pops in some cases
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Hugo Herbelin proposed to modify directly the function
"check_correct_par" to simplify commit c12b430
(see the pullrequest's discussion).
Note that the constructor "LocalNonPar" has now three arguments (instead
of two). In LocalNonPar (n,i,l) n denotes the position among real
arguments (ie. ignoring letins), i is the rel index of the expecting argument
in the context of parameters and l is the index of the inductive.
|
| |\| |
|
| | |
| |
| |
| | |
This is necessary for the patch for #4221 (817308ab5) to work.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| | | |
|
| | |
| |
| |
| |
| | |
hash-consing, so as to avoid having too many kinds of equalities with
same name.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
constant/inductive/constructor kernel_name pairs rather than viewing
them from only the user or canonical part.
Hopefully more uniformity in Constr.hasheq (using systematically == on
subterms).
A semantic change: Cooking now indexing again on full pairs of kernel
names rather than only on the canonical names, so as to preserve user
name.
Also, in pair of kernel names, ensuring the compact representation is
used as soon as both names are the same.
|
| | |
| |
| |
| |
| |
| | |
The hash function exported by the interface ought to respect the equality.
Therefore, we only use the syntactic hash for the hashconsing module while
using the canonical hash in the API.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
compatible with a unique bound module name counter which is not
synchronous with the backtracking).
We changed hash-consing of kernel name pairs to a purely memory
management issue, not trying to exploit logical properties such as
"syntactically equal user names have syntactically same canonical
names" (which is true in a given logical session, but not in memory,
at least because of residual values after backtracking).
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| | |
I was not seeing the warning due to the 10 deprecation warnings before
it...
|
| |\| |
|
| | |
| |
| |
| |
| | |
We were throwing away constraints from 'with Definition' in module
type ascriptions.
|
| | |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
Stuck primitive projections were never convertible.
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| | |
- Proper [family] implementation
- Use the tailor made hash function for Sorts.t in two places.
|
| | |
| |
| |
| |
| | |
We lambda-lift by hand the graph traversal functions in Univ to allocate
less closures.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| | |
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
| | |
| |
| |
| | |
This is my attempt at understanding each case and subfunction of the positivity check and document each of them to the best of my capacity.
|
| |\| |
|
| | |
| |
| |
| |
| | |
Nothing is done for camlp4
There is an issue with computing camlbindir
|
Maxime Dénès
Catalin Hritcu
Pierre-Marie Pédrot
Gregory Malecha
mlasson
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Arnaud Spiwack
Pierre Boutillier