diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-06 13:29:18 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-07 09:11:46 +0100 |
| commit | 3308336f1a412cb2a218e3a70a171cb7ff88bfbe (patch) | |
| tree | 17b948277e19f5c15998dd901e67235e6ffe6897 /test-suite/output/Arguments_renaming.v | |
| parent | d6a18782919367006ab1cee0a5577ed9b3028682 (diff) | |
Fix #5182: "Arguments names must be distinct." is bogus and underinformative
Diffstat (limited to 'test-suite/output/Arguments_renaming.v')
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 2d14c94ac..0cb331347 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -47,7 +47,7 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. -Fail Arguments eq_refl {F F}, [F] F. +Fail Arguments eq_refl {F F}, [F] F : rename. Fail Arguments eq {F} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. |