| Age | Commit message (Collapse) | Author |
|---|
|
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 [ ].
|
|
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`.
|
|
This was already possible manually using "{ _ }" in the type of
declaration. This was also possible for type classes. So, no reason to
forbid in Arguments.
|
|
|
|
|
|
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
|
It seems warnings are not taken into account in output/
tests.
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16641 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14827 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Implicit arguments can be mentioned anonymously:
Arguments map {_ _} f l.
- To rename implicit arguments, the ": rename" flag must be used:
Arguments map {T1 T2} f l : rename.
Without the ": rename" flag arguments can be used to assert
that a function has indeed the expected number of arguments and
that the arguments are named as expected.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Example:
Arguments eq_refl {B y}, [B] y.
Check (eq_refl (B := nat)).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
