| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Originally, "VernacTime" and "VernacRedirect" were defined like this:
type vernac_expr =
...
| VernacTime of vernac_list
| VernacRedirect of string * vernac_list
...
where
type vernac_list = located_vernac_expr list
Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:
| VernacTime of located_vernac_expr
| VernacRedirect of string * located_vernac_expr
which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.
|
| |\ |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
The name in the return clause has no semantic meaning, we must not
look at it.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
It will later be used to fix a bug and improve some code.
Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
|
| | |
| |
| |
| |
| | |
next to each other, waiting for possible integration into a more
uniform API.
|
| |\| |
|
| | |
| |
| |
| |
| | |
constraints at the time of Next Obligation/Solve Obligations so that
interleaving definitions and obligation solving commands works properly.
|
| | |
| |
| |
| |
| |
| |
| | |
using the wrong context.
This is very bad style but currently unavoidable, at least we don't
throw an anomaly anymore.
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
non-polymorphic definitions, original universes might be substituted
later on due to constraints.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
instances for each of the inductive in the same block but reuse the
original universe context shared by all of them. Also do not force
schemes to become universe polymorphic.
|
| |\| |
|
| | |
| |
| |
| |
| | |
definition, if they manipulate structures depending on the initial state
of the context.
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
When a future is fully forced (joined), the fix_exn is dropped,
since joined futures are values (hence they cannot raise exceptions).
When a future for a transparent definition enters the environment
it is joined. If one needs to pick its fix_exn, he should do it
before that.
|
| | |
| |
| |
| | |
involving Futures.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| | |
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
| | | |
|
| | |
| |
| |
| | |
structure.
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
When F is a Functor, doing an 'Include F' triggers the 'Include Self'
mechanism: the current context is used as an pseudo-argument to F.
This may fail with a subtype error if the current context isn't adequate.
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
This was a trivial overlook.
|
| |\| |
|
| | |
| |
| |
| |
| | |
Used to replace the standard conversion by the VM. Not so useful, and
implemented using a bunch of references inside and outside the kernel.
|
| | | |
|
| | | |
|
| |\| |
|
Matej Kosik
Pierre-Marie Pédrot
Maxime Dénès
Enrico Tassi
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Guillaume Melquiond
Pierre Letouzey