| Age | Commit message (Collapse) | Author |
|---|
|
a context.
Reviewed-by: mattam82
|
|
Reviewed-by: ejgallego
|
|
Fixes #11661
|
|
We arbitrarily use max_int as higher level of custom entries in
printing, which should be ok since only < and <= are used to decide
when to use coercions.
|
|
It is the duty of the caller to properly declare monomorphic global
constraints when creating a non-globref hint. All callers were already
abiding by this convention.
|
|
from initial evars
Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
in collections
Reviewed-by: gares
Ack-by: Zimmi48
|
|
This is to be removed once #12920 is merged.
|
|
Fix #12887
|
|
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 [ ].
|
|
|
|
Fix #12930
|
|
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.
|
