| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Ack-by: SkySkimmer
|
|
We fix a clear coding mistake in
79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 that forgot to update the
type of the parameter entry when saving mutual definitions without a
body.
We follow the solution suggested by Hugo Herbelin and drop the
type used in `start_proof`. Note the duplication here indeed.
Fixes #12895
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
Fix #13162
|
|
This improves the error message on the example for #13171, however we
may question whether there should be an error at all.
|
|
|
|
The (old) original model for notations was to associated both a
parsing and a printing rule to a notation.
Progressively, it become more and more common to have only parsing
notations or even multiple expressions printed with the same notation.
The new model is to attach to a given scope, string and entry at most
one either only-parsing or mixed-parsing-printing rules + an
arbitrarily many unrelated only-printing rules.
Additionally, we anticipate the ability to selectively
activate/deactivate each of those.
This allows to fix in particular #9682 but also to have
more-to-the-point warnings in case a notation overrides or partially
overrides another one.
Rules for importing are not changed (see forthcoming #12984 though).
We also improve the output of "Print Scopes" so that it adds when a
notation is only-parsing, only-printing, or deactivated, or a
combination of those.
Fixes #4738
Fixes #9682
Fixes part 2 of #12908
Fixes #13112
|
|
This is to be consistent with the use of parentheses in the syntax of
Notation and to support a list of attribute afterwards.
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
The current implementation of par: is still in the STM, but is optional.
If the STM does not take over it, it defaults to the implementation of
in comTactic which is based on all: (i.e. sequential).
This commit also moved the interpretation of a tactic from g_ltac to
vernac/comTactic which is more appropriate.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
specific format.
Reviewed-by: ejgallego
|
|
|
|
|
|
Used only by implicit_quantifiers
|
|
-> "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 [ ].
|
|
|
