index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
Arguments_renaming.out
Age
Commit message (
Expand
)
Author
2021-01-13
Make sure "Print Module" write a dot at the end of inductive definitions.
Guillaume Melquiond
2020-08-28
About: Add a mention that arguments have been renamed, if ever it is the case.
Hugo Herbelin
2020-08-28
Where there are several lists of implicit arguments, don't pretend names matter.
Hugo Herbelin
2020-08-28
Do not write "rename" for arguments in About, since these arguments are valid...
Hugo Herbelin
2020-08-28
When printing the type in About, use the renamed arguments.
Hugo Herbelin
2020-08-28
When reporting an implicit argument error on a rename argument, use the renam...
Hugo Herbelin
2020-08-28
In "About", print all arguments, even if it is trailing list of _.
Hugo Herbelin
2020-08-19
Do not refresh the names of implicit arguments.
Jasper Hugunin
2020-04-15
Add needed commas in message
Jim Fehrle
2020-03-18
Change some ouput tests due to the printing of implicits
SimonBoulier
2020-02-13
Arguments: removing the restriction to set an anonymous parameter implicit.
Hugo Herbelin
2019-11-20
Combine similar arguments when printing Arguments command
Gaëtan Gilbert
2019-10-31
restore red behaviour printing
Gaëtan Gilbert
2019-10-31
Fix output tests
Gaëtan Gilbert
2019-05-10
Remove various circumvolutions from reduction behaviors
Maxime Dénès
2019-02-28
Implement a method for manual declaration of implicits.
Jasper Hugunin
2019-01-09
Stop [Print] from saying [is (not) universe polymorphic].
Gaëtan Gilbert
2018-12-17
Stop printing Monomorphic/Polymorphic in Print.
Gaëtan Gilbert
2018-11-02
Remove is_universe_polymorphism from printing
Gaëtan Gilbert
2018-10-04
Test-suite: avoid explicit references to “Top”
Vincent Laporte
2018-05-25
An attempt to clarify error message for Arguments needing "rename" flag.
Hugo Herbelin
2018-02-22
Adding mention of shelved/given-up status in "Show Existentials".
Hugo Herbelin
2017-03-21
[pp] Make feedback the only logging mechanism.
Emilio Jesus Gallego Arias
2016-11-07
Fix #5182: "Arguments names must be distinct." is bogus and underinformative
Maxime Dénès
2016-10-27
Add missing dot to impargs error message.
Maxime Dénès
2016-10-27
Complete overhaul of the Arguments vernacular.
Maxime Dénès
2016-09-30
Ignore file names in warning emitted by test-suite/output/* (#5111)
Enrico Tassi
2016-09-29
Arguments: cleanup + detect discrepancy rename/implicit (#3753)
Enrico Tassi
2016-06-16
Not taking arguments given by name or position into account when
Hugo Herbelin
2015-03-09
Do not display the status of monomorphic constants unless in universe-polymor...
Guillaume Melquiond
2015-03-05
Fix testsuite with respect to the new formatting of Fail messages.
Guillaume Melquiond
2014-10-03
Adapting output/Arguments_renaming continued.
Hugo Herbelin
2014-10-02
Adapting output/Arguments_renaming.out after fixing printing of
Hugo Herbelin
2014-08-12
Upgrading output tests.
Hugo Herbelin
2014-05-08
Fixing output test-suite: since universe polymorphism, the Print command
Pierre-Marie Pédrot
2014-02-28
Fix output test-suite 'simpl tactic' -> 'reduction tactics'
Pierre Boutillier
2013-11-03
test-suite fixup
pboutill
2013-07-29
better error message for unexpected renaming (closes #2987)
gareuselesinge
2012-03-02
Noise for nothing
pboutill
2011-12-19
Arguments: check rename even if no implicit is specified
gareuselesinge
2011-12-17
Command Arguments: standardizing format of error messages and American spelling.
herbelin
2011-12-06
Minor fixes to Arguments
gareuselesinge
2011-11-21
Renamig support added to "Arguments"
gareuselesinge
