diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-03 09:01:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-03 09:02:02 +0200 |
| commit | df0d30099a9647e681391c15bac12655819772ce (patch) | |
| tree | 3d60327c20348c9b741b966f447072ac4fd2733e /test-suite/output/Arguments_renaming.out | |
| parent | a0e47bcf277d11ec7d2272bc5167fee898ad9016 (diff) | |
Adapting output/Arguments_renaming continued.
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index dbc1b4a21..c29f56494 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -103,7 +103,7 @@ The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.myplus -myplus +@myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: => Error: All arguments lists must declare the same names. |