| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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.
|
|
|
|
The request for positivity to be assumed is honored.
|
|
The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.
|
|
positivity is assumed.
|
|
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
|
|
Was making the study of bugs like #4139 painful.
Now printing a better error message when a compiled file is missing.
|
|
|
|
Patch provided by Çagdas Bozman.
|
|
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
|
Instead of checking if the native compiler directory exists before creating it,
we simply create it by default and catch the potential exception due to its
presence.
|
|
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
|
Oups, sorry, I should have compiled the stdlib in full. Not only
the ~polyprop wasn't propagated properly, but Matthieu made it be
false by default somewhere instead of true. Argl...
|
|
The ~polyprop argument wasn't propagated properly anymore,
leading the extraction to try to operate on situations it cannot
handle (yet). Cf Table.error_singleton_become_prop for more details.
Regression test added.
|
|
|
|
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
|
The solution is a bit ugly. In order for two tactic notations identifiers not
to be confused by the inclusion from two distinct modules, we embed the name of
the source module in the identifiers. This may still fail if the same module is
included twice with two distinct parameters, but this should not be possible
thanks to the fact any definition in there will forbid the inclusion, for it
would be repeated. People including twice the same empty module otherwise
probably deserve whatever will arise from it.
|
|
|
