| Age | Commit message (Collapse) | Author |
|---|
|
specific format.
Reviewed-by: ejgallego
|
|
|
|
-> "constr"
Reviewed-by: herbelin
Ack-by: Zimmi48
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
It was not documented, not properly tested and thus likely buggy. Judging
from the code alone I spotted already one potential bug. Further more it was
prominently making use of the infamous "arbitrary term as hint" feature.
Since the only user in our CI seems to be a math-classes file that introduced
the feature under a claim of "cleanup", I believe we can safely remove it
without anyone noticing.
|
|
Became unused in e034b4090ca45410853db60ae2a5d2f220b48792
|
|
Fix #13109
|
|
|
|
candidates.
We also show the incompatible contender.
Ideally, we should also remember the source of the other contender.
|
|
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
|
