| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
for which there corresponding tag are greater than max_variant_tag.
The code is a merge with the patch proposed by Bruno on
github barras/coq
commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c
|
|
and 8388851 non-constant constructor.
|
|
change the representation of inductive constructor
when there is too many non constant constructors in the inductive type
Conflicts:
kernel/cbytegen.ml
|
|
more than 245 constructors (unsupported by OCaml's runtime).
|
|
Module substitution is made nodewise, allowing to drop it for opaque terms
in the VM. This saves a few useless substitutions.
|
|
presence of let-ins and recursively non-uniform parameters).
The bug was in the List.chop of Inductiveops.get_arity which was wrong
in the presence of let-ins and recursively non-uniform parameters.
The bug #3491 showed up because, in addition to have let-ins, it was
wrongly detected as having recursively non-uniform parameters.
Also added some comments in declarations.mli.
|
|
presence of let-ins. This fixes #3491.
|
|
Parameters were missing in the context, apparently without negative
effects because the context was used only for whd normalization of
types, while reduction (in closure.ml) was resistant to unbound rels.
See however next commit for an indirect effect on the wrong
computation of non recursively uniform parameters producing an anomaly
when computing _rect schemas.
|
|
|
|
Backported from a patch for v8.4 by Pierre Chambart. Part of the commit has been rendered obsolete by code reorganisation, leaving:
* OCaml runtime header files used to declare the int32, uint32, int64
and uint64 type. That got removed, and uses of those types should be replaced by the standard ones: uint32_t, int32_t, int64_t, uint64_t. Those are defined in stdint.h.
|
|
cases, in some cases.
|
