| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
For discharging it is important that constants occur in the libstack
in an order that respects the dependencies among them. This is
impossible to achieve for private constants when they are exported globally
without this (ugly IMO) api.
|
|
|
|
Universe instances for constructors were not always correct, for instance in:
[cons _ list (nil _)] with a polymorphic [list] type, [nil] was receiving an
empty instance.
|
|
- Universes are now represented in the VM by a structured constant containing the
global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
constructor arguments, which has to be prevented.
Was showing up for instance when evaluating [cons _ list (nil _)] with
a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.
Patch written with Benjamin Grégoire.
|
|
Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.
|
|
|
|
|
|
polymorphic definitions.
- This implementation passes universes in separate arguments and does not
eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
|
|
|
|
|
|
After all, let's target 8.6.
|
|
This makes sense probably on Windows too, to be evaluated, maybe .exe
suffix should be added.
|
|
Since the functions of this plugin exit by raising exceptions, globing
was never restarted. This prevented coqdoc from generating a proper
output whenever some feature of this plugin was used. There does not seem
to be any parsing of dynamic expressions, so pausing globing does not make
much sense in the first place.
|
|
|
|
structure.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
paths for ocaml* executables in the generated config/Makefile.
Hoping I'm not doing something wrong. E.g., I don't see why it would
not be ok for windows or macosx too, since e.g. camlp5o was already
with a full path.
|
|
- usage ill-formed for -native-compiler
- compatibility with the configure of 8.4 (-force-caml-version),
though e.g. its force-ocaml-version alias is no longer supported
(but at the same time not documented either, so...)
|
|
are redhibitory.
|
|
|
|
|
|
|
|
|
|
Entries defined in the Pcoq AST of symbols must be marshallable, because they
are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as
they contain functional values. This is why the Pcoq module used a pair
[string * string] to describe entries. It is obviously type-unsafe, so
we define a new abstract type in its own module. There is a little issue
though, which is that our entries and CAMLP4/5 entries must be kept
synchronized through an association table. The Pcoq module tries to
maintain this invariant.
|
|
As shown by the code snippets in these bug reports, I've been too
hasty in considering these situations as anomalies in commit 466c4cb
(at least the one at the last line of consistency_checks). So let's turn
these anomalies back to regular user errors, as they were before this commit.
|
|
|
|
|
|
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.
|
|
|
|
For instance, "Hint Resolve (fst _ _)." was looping (bug in 841bc461).
|
|
by the type to prove (was introduced in 35846ec22, r15978, Nov 2012).
Not only it does not work when exact is called via a Ltac definition,
but, also, it does not scale easily to refine which is a TACTIC
EXTEND.
Ideally, one may then want to propagate scope interpretations through
ltac variables, as well as supporting refine...
See #4034 for a discussion.
|
|
|
|
Was introduced in b06d3badb (15 Jul 2015).
|
|
This removes 109 Obj.magic in one patch!
|
