| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: JasonGross
Reviewed-by: ejgallego
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
This lets us remove the closure passing for the program inference_hook
|
|
|
|
Proof entries are low-level objects and should not be manipulated by
users directly, in particular as we want to unify all the code
around declaration of constants.
This patch doesn't bring by itself a lot of improvement, other than
setting the base where to extend the interface, however it already
points out some points of interest, and in particular the manipulation
of opacity done by `Derive` which can be quite problematic, and of
course the handling of delayed proofs.
So while this is a first step, IMHO it doesn't harm a lot having it in
place, but a lot more work will be needed, in particular regarding the
handling of delayed proofs.
To make `proof_entry` a fully abstract type, the remaining work is
focused on `abstract` and obligations, both of which do quite a few
hackery that will have to be migrated to the `Declare` API.
|
|
We factor some duplicate code, this is a step towards making the
`proof_entry` type abstract.
|
|
vernac/
Ack-by: Janno
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
This is useful to remove some duplicate bits in other declare files.
|
|
|
|
Patch suggested by Gaëtan Gilbert
|
|
The code is self-contained and only used by commands; this also
highlights the several `Libobject.obj` registered for each
declaration.
|
|
The code is self-contained and only used by commands; this also
highlights the several `Libobject.obj` registered for each
declaration.
|
|
|
|
If you have access to a kernel name you also should have the
environment in which it is defined, barring hacks. In order to
disfavor hacks we make the standard lookups raise anomalies so that
people are forced to admit they rely on the internals of the
environment.
We find that hackers operated on the code for side effects, for
finding inductive schemes, for simpl and for Print Assumptions. They
attempted to operate on funind but the error handling code they wrote
would have raised another Not_found instead of being useful.
All these uses are indeed hacky so I am satisfied that we are not
forcing new hacks on callers.
|
|
There are no more users.
|
|
|
|
|
|
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
This allows UI clients to implement a different state management
strategy with regards to proofs, and in particular to override
`Vernacinterp.interp`.
This is work in progress towards having a true `VtTactic` which shall
not perform any state changes non-functionally, and actually removing
the series of `assert false` due to meta-vernacs.
|
|
|
|
The general idea is to move tests on scope=Discharge and on
Lib.sections_are_opened up in the call stack. This allows better
control over the universe manipulation.
There are some corner case behaviour change, eg:
- [Context (foo:=bla)] outside a section correctly declares an
axiom (fix #10668)
- (not observable) universes for [Variable A B : Type] in section are declared only once
- universes and universe names for [Axiom A B : Type] are declared
only once. This changes the qualification of the universe name:
before it was the last axiom (so [B.u0]), now it's the first
one ([A.u0]).
Probably nobody cares about this.
- context outside section uses different [kind]
I'm not sure why context outside a section behaves differently based
on whether we're in a module type, I tried to preserve it but maybe we
should uniformize.
The universe manipulation for Axiom (in the declare_assumptions
function) is a bit awkward, maybe when there are multiple monomorphic
axioms instead of trying to attach the universes to the first one we
should just declare them separately like with Context. OTOH unlike
with context dropping the universe names seems incorrect.
|
|
Primitives don't have anything to do with assumptions.
|
|
(letins still declare universes in declare_variable as they use
entries)
The section check_same_poly is moved to declare_universe_context (it
makes more sense there, universe polymorphism doesn't apply to the
variables/letins themselves)
|
|
We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.
Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.
|
|
sections
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
|
|
Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.
Improvement suggested by Gaëtan Gilbert.
|
|
We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.
This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.
The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.
This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
|
|
This helps extraction by not building sigT which can lower to Prop by
template polymorphism.
Bug #10757 can probably still be triggered by using module functors to
hide that we're using Prop from Program Fixpoint but that's probably
unfixable without fixing extraction vs template polymorphism in
general.
In passing we notice that Program doesn't know how to telescope SProp
arguments, we would need a bunch of variants of sigma types to deal
with it (or use Box?) so let's figure it out some other time.
We also reuse the universe instance to avoid generating a bunch of
short-lived universes in the universe polymorphic case.
|
|
|
|
`Import` does not actually need to register an object, only `Export`
does. So we specialize and rename the object into `ExportObject`.
|
|
Libraries are now handled like other modules.
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: maximedenes
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
This is step 1 on removing library state from the lower layers.
Here we move library loading to the vernacular layer; few things
depend on it:
- printers: we add a parameter for those needing to access on-disk data,
- coqlib: indeed a few tactics do try to check that a particular
library is loaded; this is a tricky part. I've replaced that for a
module name check, but indeed this is fully equivalent due to
side-effects of `Require`. We may want to think what to do here.
A few other minor code movements were needed, but there are
self-explanatory.
|
|
proof data on top of declare.
Reviewed-by: ppedrot
|
|
As documented in the feedback API.
|
|
Non-delayed entries can be done with the current constructor, delayed
ones will require more work.
|
|
top of declare.
This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.
This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.
This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.
A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.
Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
|
|
Fix changelog entry
Fix build of the user manual
Markup fixes from Théo Zimmermann
Update doc and changelog and improve error messages.
|
