| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| | | |
|
| |/ |
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
records for cbv and native_compute
|
| | | |
| | |
| | |
| | | |
Fixes #5286 (last remaining part).
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We separate functions dealing with VM values (vmvalues.ml) and
interfaces of the bytecode interpreter (vm.ml). Only the former relies
on untyped constructions.
This also makes the VM architecture closer to the one of native_compute,
another patch could probably try to share more code between the two for
conversion and reification (not trivial, though).
This is also preliminary work for integers and arrays.
|
| |\ \
| | |
| | |
| | | |
for primitive projections
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
The constant_value function was actually not behaving the same as
constant_value_in w.r.t. projections. The former was not used, and
the only place that used the latter was in Tacred and was statically
insensitive to the use of projections.
|
| | | | |
|
| |/ / |
|
| | |
| |
| |
| |
| |
| |
| | |
We simply use a record and pack the rel and var substitutions in it. We also
properly compose variable substitutions.
Fixes #6534: Fresh variable generation in case of clash is buggy.
|
| | |
| |
| |
| |
| |
| | |
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
|
| |/ |
|
| |
|
|
|
|
| |
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
Typeclasses.typeclass
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
| |\ \ |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | | |
Universe instances were lost during constructions of the canonical instance.
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
same right-hand side.
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
arguments.
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.
Thanks to @SkySkimmer for lots of comments and bug-finding.
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.
Adding options
Unset Printing Allow Default Clause.
to deactivate the second behavior, and
Unset Printing Factorizable Match Patterns.
to deactivate the first behavior (deactivating the first one
deactivates also the second one).
E.g. printing
match x with Eq => 1 | _ => 0 end
gives
match x with
| Eq => 1
| _ => 0
end
or (with default clause deactivates):
match x with
| Eq => 1
| Lt | Gt => 0
end
More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This is to have a better symmetry between CCases and GCases.
|
| | | | | |_|/ /
| | | |/| | |
| | | | | | |
| | | | | | | |
This is a follow-up on 866b449c497933a3ab1185c194d8d33a86c432f2.
|
| | |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The exception needs to carry aroud a pair of `env, sigma` so printing
is correct. This gets rid of a few global calls, and it is IMO the
right thing to do.
While we are at it, we incorporate some fixes to a couple of
additional printing functions missing the `env, sigma` pair.
|
| | |/ / / /
|/| | | |
| | | | |
| | | | | |
And some code simplification.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| |_|_|/ / /
|/| | | | | |
|
| | |/ / / /
|/| | | | |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | | |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| | | | |
| | | |
| | | |
| | | | |
They were not used anymore since the previous patches.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This was dead code, probably due to the fact it was once shared with the
kernel stack type.
|
| |/ / /
| | |
| | |
| | |
| | | |
It was actually not used. The only place generating one was easily writable
without it.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The patch has three parts:
- Introduction of a configure flag `-bytecode-compiler (yes|no)`
(due to static initialization this is a configure-time option)
- Installing the hooks that register the VM with the pretyper and the
kernel conditionally on the flag.
- Replacing the normalization function in `Redexpr` by compute if the
VM is disabled.
We also rename `Coq_config.no_native_compiler` to `native_compiler`
and `Flags.native_compiler` to `output_native_objects` [see #4607].
|
| |/ /
| |
| |
| |
| |
| |
| |
| | |
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
|
| |\ \
| | |
| | |
| | | |
#3125)
|
| | |/
|/| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This function returns InProp or InSet for inductive types only when
the inductive type has been explicitly truncated to Prop or
(impredicative) Set.
For instance, singleton inductive types and small (predicative)
inductive types are not truncated and hence in Type.
|
| | |
| |
| |
| | |
recursive functions.
|
| |\ \ |
|
| | |/
|/|
| |
| |
| | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| | |
| |
| |
| | |
Also nicer error when the constraints are impossible.
|
Maxime Dénès
Gaëtan Gilbert
Pierre-Marie Pédrot
Cyprien Mangin
Emilio Jesus Gallego Arias
Hugo Herbelin
Théo Zimmermann
Matthieu Sozeau