diff options
| author | Pierre-Marie Pédrot | 2014-05-08 15:31:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-08 15:35:59 +0200 |
| commit | 0cebd2b86a90cc1361bcfac6bb097540e22c9a21 (patch) | |
| tree | 648ece59fd72185da10d71771d9f858aa1fa7fd4 /dev | |
| parent | 6a3767e48e91604071b5709a6658aa2f255a4522 (diff) | |
Fixing output test-suite: since universe polymorphism, the Print command
shows the polymorphism status of the term.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions