| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: jashug
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
Ack-by: SkySkimmer
|
|
Fix #12928
Fix #3146
|
|
Close #5703
I have no idea when this got fixed.
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
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.
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
The purpose of `NsatzTactic` is to allow using `nsatz` without the
dependency on real axioms. So we declare the instances for `Z` and `Q`
in that file, so that users don't have to re-create them.
Fixes #12860
|
|
Fix #12676
|
|
Fix #12889
|
|
documentation
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: jfehrle
|
|
Reviewed-by: mattam82
Ack-by: ppedrot
|
|
of artificial dependencies disappearing by reduction
Reviewed-by: ppedrot
|
|
|
|
We fix it by reducing K-redexes the same in the both places
(make_tuple and minimal_free_rels) which compute the dependencies of a
dependent equality.
|
|
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`.
|
|
test files.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
Fix #7015
|
|
This is a companion to #12479 as per
https://github.com/coq/coq/pull/12479#issuecomment-641336039 that
changes some of the PrimFloat notations:
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
We also put them in a module, so users can `Require PrimFloat. Import
PrimFloat.PrimFloatNotations` without needing to unqualify the
primitives.
Fixes the part of #12454 about floats
|
|
Helps with #12566
|
|
Reviewed-by: herbelin
|
|
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.
|
|
projection
Reviewed-by: ejgallego
Ack-by: gares
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
Reviewed-by: ejgallego
|
|
Fix #12651
|
|
Perhaps we should thread an evar map with the Var universes added
through to cs_pattern_of_constr but that would be significantly more invasive.
Fix #12528
|
|
|
|
We interpret `{|proj=pat|}` as `@C _ pat` instead of `C _ pat` (where
the `_` stands for the parameters).
Fix #12534
|
|
Fix #12551
|
|
patterns.
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
|
|
Fixes #12571.
|
|
|
|
|
|
Fixes #12529
|
|
|
|
Fixes #12390
|
|
This is a quick fix to avoid the anomaly, with a fallback on before
b1b8243b7fc.
|
|
Reviewed-by: ppedrot
|
|
eta-expansion of "match" branches
Reviewed-by: gares
Ack-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: anton-trunov
Reviewed-by: ejgallego
|
|
runtime.
Reviewed-by: herbelin
|
|
|
|
See #11840 for a motivation. I had to fix Floats.FloatLemmas because
it uses the same name for a notation and a term, and the fact this
unfold was working on this was clearly a bug. I hope nobody relies
on this kind of stuff in the wild.
Fixes #5764: "Cannot coerce ..." should be a runtime error.
Fixes #5159: "Cannot coerce ..." should not be an error.
Fixes #4925: unfold gives error on Admitted.
|
