diff options
| author | Maxime Dénès | 2020-08-20 16:32:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-20 16:32:33 +0200 |
| commit | 609152467f4d717713b7ea700f5155fc9f341cd7 (patch) | |
| tree | 97696e08209c7990344319e7b2d20a459140f5c4 /test-suite/output | |
| parent | b409b9837ce438042bb259d16a1b5156a2e0acb9 (diff) | |
| parent | 300157fc6176856f3f792d956925af366ef3329e (diff) | |
Merge PR #12756: Do not refresh the names of implicit arguments.
Reviewed-by: herbelin
Reviewed-by: maximedenes
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 1 | ||||
| -rw-r--r-- | test-suite/output/Implicit.out | 2 |
3 files changed, 1 insertions, 4 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e0aa758812..c28bb14eb3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -84,8 +84,6 @@ Argument lists should agree on the names they provide. The command has indeed failed with message: Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Some argument names are duplicated: F -The command has indeed failed with message: Argument number 3 is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 6ac09cf771..6001850046 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -48,7 +48,6 @@ 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 : rename. Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index ef7667936c..2265028d3e 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments d2 [x x0]%nat_scope +Arguments d2 [x x]%nat_scope map id (1 :: nil) : list nat map id' (1 :: nil) |