| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
obligations".
|
| | |
|
| | |
|
| |
|
|
| |
Also register properly the kind of definition.
|
| |
|
|
|
|
|
|
| |
When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
|
| |
|
|
| |
so that they are not silently computed when not in debugging mode.
|
| |
|
|
|
|
| |
Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
|
| |
|
|
| |
The user-provided sort was ignored for them.
|
| |
|
|
|
| |
As if we were adding : Type. Consistent with inductives with no
declared arity.
|
| |
|
|
| |
Forcefully equating it to the inferred level is not always desirable or possible.
|
| | |
|
| |
|
|
| |
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
| | |
|
| |
|
|
| |
multiple patterns.
|
| | |
|
| |
|
|
|
|
| |
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
|
| |
|
|
| |
Fixpoint/Definition.
|
| |
|
|
|
|
|
| |
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The previous behavior was to include the interface of such a functor,
possibly leading to the creation of unexpected axioms, see bug report #3746.
In the case of non-functor module with restricted signature, we could
simply refer to the original objects (strengthening), but for a functor,
the inner objects have no existence yet. As said in the new error message,
a simple workaround is hence to first instantiate the functor, then include
the local instance:
Module LocalInstance := Funct(Args).
Include LocalInstance.
By the way, the mod_type_alg field is now filled more systematically,
cf new comments in declarations.mli. This way, we could use it to know
whether a module had been given a restricted signature (via ":"). Earlier,
some mod_type_alg were None in situations not handled by the extraction
(MEapply of module type).
Some code refactoring on the fly.
|
| | |
|
| |
|
|
|
| |
The name in the return clause has no semantic meaning, we must not
look at it.
|
| |
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
context to the reduction function. Fixes MapleMode.
|
| |
|
|
|
| |
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
|
| |
|
|
| |
definitions.
|
| |
|
|
|
|
| |
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
|
| | |
|
Pierre-Marie Pédrot
Guillaume Melquiond
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Maxime Dénès
Pierre Letouzey
Enrico Tassi