| Age | Commit message (Collapse) | Author |
|---|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
If a return type is given to a match/if/let, then we are in context
(and thus may skip coercions or not make explicit those implicit
arguments inferable from context). Note that the notion of "inferable
from context" remains anyway an approximation in the case of implicit
arguments.
The body of a fix/cofix is also in context.
Also fixed an inconsistency with parsing in the scope used to print
the body of a fix.
|
|
Compared to the original proposition (59a594b in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
|
Fixing output tests after having added flushing of warning in
revisions 14747 and 14750.
Moving Implicit output test to new command Arguments.
Adding test of new Arguments syntax in PrintInfos.v.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
arguments needed for correct typing of partial applications (knowing
that in practice, users should anyway better declare such arguments as
maximally inserted).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14404 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
discussion avec Georges)
- La notion d'insertion maximale n'est plus globale mais attachée à
chaque implicite
- Correction de petits bugs dans le calcul des implicites
- Raffinement de la notion "sous contexte" pour l'affichage des coercions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4585 85f007b7-540e-0410-9357-904b9bb8a0f7
|
