michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/bad_coercions): expected output

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-05 02:52:09 -07:00
parent d731a4ab13
commit bebe8a4f17
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/bad_coercions.lean.expected.out
View file

@ -1,2 +1,2 @@
bad_coercions.lean:12:18: error: invalid '[coercion]' attribute, coercions cannot be defined in contexts
bad_coercions.lean:18:16: error: invalid '[coercion]' attribute, coercions cannot be defined in contexts
bad_coercions.lean:12:18: error: invalid '[coercion]' attribute, (non local) coercions cannot be defined in contexts
bad_coercions.lean:18:16: error: invalid '[coercion]' attribute, (non local) coercions cannot be defined in contexts