| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
quotations at printing time
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
applications in notations
Reviewed-by: ejgallego
Ack-by: maximedenes
|
|
|
|
Also pass `--output-sync` on the CI, as suggested in
https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect
against this failure mode.
Fixes #13062
|
|
|
|
The doc states it is deprecated since 1386cd9 but this was ages before the
deprecation mechanism existed.
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
We finally pass the location in the "ist", and keep it in the "VFun"
which is associated to expanded Ltac constants.
|
|
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.
|
|
- merlin.in : added zarith
- test-suite/Makefile remove .csdp.cache on make clean
updated .csdp.cache.test-suite
|
|
|
|
Keep Numeral Notation wit a deprecation warning.
|
|
The previous implementation appears to be sound when Mangle Names is
off, but it relies on two fragile assumptions, namely that
next_global_ident_away always returns different identifiers when called
with naming hints which are different after stripping all digits from
the end, and that default_id_of_sort (locally defined) never returns
"HC" or "P", or either of those followed by a string of digits.
These changes make both assumptions unnecessary.
As a side note, it seems odd that fresh is ignoring it's env parameter.
|
|
|
|
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
|
|
comment in #12944).
Ack-by: RalfJung
Ack-by: jashug
Reviewed-by: ppedrot
|
|
The test is refined to handle aliases: i.e. undefined evars coming from
restrictions and evar-evar unifications with an initial evar are not
considered fresh unresolved evars. To check this, we generalize the
restricted_evars set to an aliased_evars set in the evar map,
registering evars being solved by another evar due to restriction
or evar-evar unifications. This implements the proposal of PR #370
for testing the resolution status of evars independently of the evar-evar
orientation order.
This allows [apply] to refine an evar with a new one if it results from a
[clear] request or an evar-evar solution only, otherwise the new evar is
considered fresh and an error is raised.
Also fixes bugs #4095 and #4413.
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
|
|
maybe_unify_params_in
Reviewed-by: maximedenes
|
|
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Fix #12887
|
|
The bugs involved:
- a notation with a subterm in position of function of an application
- use of this notation in another notation creating a non-flattened application
In particular, this fooled "find_appl_head" (for #10803) and the
translation from GApp to NApp (for #9403).
We fix the translation NApp -> GApp (since glob_constr is supposed to
have its applications flattened).
|
|
Strangely, this was not yet noticed. Hiding of a scoped notation by a
lonely notation should be checked at printing time.
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
Fix #12944
|
|
The names computed in consume_pattern were lost when calling
intros_pattern_core. Moreover, the computation of names to avoid was
done several time. We compute it once for all.
|
|
Reviewed-by: jashug
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
Ack-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
Should be more robust with async proofs
|
|
Fix #12928
Fix #3146
|
|
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 [ ].
|
|
|
|
Close #5703
I have no idea when this got fixed.
|
|
Fix (partial) #5502
|
|
Fix #12930
|
|
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
Ack-by: SkySkimmer
|
|
arguments of notations
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
We used to be refreshing the names for intros but not using the
refreshed names. The same pattern of `intro_using` (which is what
`intros ?name` effectively is) messing things up as in coq/coq#12881.
|
|
|
