| Age | Commit message (Collapse) | Author |
|---|
|
Before this patch, the proof engine had three notions of shelves:
- A local shelf in `proofview`
- A global shelf in `Proof.t`
- A future shelf in `evar_map`
This has lead to a lot of confusion and limitations or bugs, because
some components have only a partial view of the shelf: the pretyper can
see only the future shelf, tactics can see only the local and future
shelves. In particular, this refactoring is needed for #7825.
The solution we choose is to move shelf information to the evar map, as
a shelf stack (for nested `unshelve` tacticals).
Closes #8770.
Closes #6292.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
- take just a ugraph instead of the whole env
- rename to update_sigma_univs
- push global env lookup a bit further up
- fix vernacinterp call to update all surrounding proofs, not just the
top one
- flip argument order for nicer partial applications
|
|
See https://github.com/coq/coq/pull/12875#issuecomment-679190489.
|
|
That is, in "About", use _ for the variables of the extra lists.
See discussion at https://github.com/coq/coq/pull/12875#issuecomment-679190489.
|
|
validated.
|
|
|
|
renaming.
Example:
> Arguments id [B] {b} : rename.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Argument B is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
|
|
|
|
We remove some dead aliases and add some documentation to the
interface file.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene
|
|
|
|
|
|
|
|
Add a mli file and uniformize indentation on the way.
|
|
The fix is a missing check of equality of custom entries. The enhancements are:
- not to bother breaking hints
- not to care about the border or internal position when the level is
made explicit
Ideally, one could also improve the treatment of DefaultLevel. To be
done later on.
|
|
Fix #12688.
Original test:
~~~coq
Record my_mod: Type := mk { datatype: Type; }.
Print Universes Subgraph (my_mod.u0). (* OK *)
From ITree Require Export ITree. (* using coq-itree for the sake of example *)
Print Universes Subgraph (my_mod.u0). (* Runs forever (> 1 min) *)
~~~
The issue is that we produce a subgraph with the user-given universes
+ Set and Prop. In the test the user given universes are not connected
to other universes, but Set is below every universe so we traverse the
whole graph.
We can go faster by just checking whether Set is strictly below each
universe we're interested in.
Maybe this would be better handled at the ugraph level but that
requires thinking about lbound so I didn't do it.
I tested locally with Require Reals, which makes the print take about
0.1s on my PC before this patch. This is enough to check that we're
now faster (near-instant) but not enough for automatic testing.
Note that the other uses of UGraph.constraints_for (for private
polymorphic universes and for context restriction) are interested in
all ambient universes so the traversals starting at Set end quickly
and do not cause the same issue.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
|
|
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
|
|
|
|
Reviewed-by: ppedrot
|
|
Defined constants
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
|
|
Helps with #12566
|
|
|
|
declaration path
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
generic printing format in anticipation of further not-only-parsing uses of the notation
Reviewed-by: ppedrot
|
|
This is a leftover after the unification of constant information,
`kind` is now correctly set by the single caller of
`Obls.add_mutual_definitions`.
|
|
Ack-by: gares
Reviewed-by: ppedrot
|
|
This is about the third time I try to kill this file but for some reason
it is still here.
|
|
Fixes #11970.
|
|
This is to anticipate further not-only-parsing uses of the notation.
|
|
This is an alternative to #12663 ; much preferable as the kind
information is already stored in the constant object.
|
|
Exceptions should not printed except for the top-level.
There is the weird anomaly-absorbing code in `Reductionops`, I wonder
how frequent that case is, but as the exception is absorbed printing
there could have a real impact.
|
|
This requires updating the parameter count at section end, I felt it
was easier to do with rebuild_function but it could be done in
discharge if needed.
Incidentally fixes #12649.
|
|
|
|
This is also needed in equations.
|
|
|
|
This is for use in Equations. At some point we should make all hook aware
of state, but this should suffice for now.
Note the comments as the role of hooks here, this may need further
cleanup indeed.
|
|
This is already taken of by `declare_definition`, by consistency with
the mutual case.
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
|
|
This is essential to allow hooks to modify state.
|
