| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| |
|
|
|
| |
- 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.
|
| |
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
| |
is reduced as if without let-in, when applied to arguments.
This allows e.g. to have a head-betazeta-reduced goal in the following example.
Inductive Foo : let X := Set in X := I : Foo.
Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
|
| |
|
|
|
|
|
|
| |
[kind_of_term].
To be able to write equality up to evar instantiation instantiation.
Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
|
| |
|
|
| |
[compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq].
|
| | |
|
| | |
|
| |
|
|
| |
do not contribute. Fixes bug #3808.
|
| |
|
|
|
| |
typecheck with definitions and thread it accordingly when typechecking
module expressions.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
safety hole in judge_of_constant_knowing parameters which was not
checking the result of the check correctly (the rest of the calls in
that file and all of the checker have been checked).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
printing functions touched in the kernel).
|
| |
|
|
|
|
|
|
| |
This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put
back in place the Requires inside modules that were found in the std lib.
Conflicts:
kernel/safe_typing.ml
|
| |
|
|
|
|
| |
match predicates for vm_compute and compile polymorphic definitions
to constant code. Add univscompute test-suite file testing VM
computations in presence of polymorphic universes.
|
| |
|
|
|
| |
One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
|
| |
|
|
|
|
|
|
|
|
| |
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
|
| |
|
|
| |
Solves an efficiency problem in Makefiles generated by coq_makefile.
|
| | |
|
Matthieu Sozeau
Pierre-Marie Pédrot
Maxime Dénès
Guillaume Melquiond
Pierre Letouzey
Arnaud Spiwack
Benjamin Gregoire
Matthieu Sozeau
Hugo Herbelin
Enrico Tassi