diff options
| author | Emilio Jesus Gallego Arias | 2020-02-20 13:59:33 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-20 13:59:33 -0500 |
| commit | 932cc10b6256396f07af2d083245b610ec842f37 (patch) | |
| tree | 2f6d013f9badaa36ba5d92b748cd3ff33977b1f7 /test-suite | |
| parent | f748ca04748ef00b85de7f31dc1dc7f0a985ec3f (diff) | |
| parent | d696eb98189eccdc2f6adb851e54af37e7f8d83b (diff) | |
Merge PR #11143: In Print/Check/Show, adopt the view that the attached type information may impact the display of coercion and implicit arguments.
Reviewed-by: ejgallego
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Implicit.out | 2 | ||||
| -rw-r--r-- | test-suite/output/NumeralNotations.out | 2 | ||||
| -rw-r--r-- | test-suite/output/NumeralNotations.v | 1 |
3 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 5f22eb5d7c..28afd06fbc 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -1,4 +1,4 @@ -compose (C:=nat) S +compose S : (nat -> nat) -> nat -> nat ex_intro (P:=fun _ : nat => True) (x:=0) I : ex (fun _ : nat => True) diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index 505dc52ebe..113384e9cf 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -75,7 +75,7 @@ The command has indeed failed with message: In environment v := 0 : nat The term "v" has type "nat" while it is expected to have type "wuint". -File "stdin", line 202, characters 2-72: +File "stdin", line 203, characters 2-72: Warning: The 'abstract after' directive has no effect when the parsing function (of_uint) targets an option type. [abstract-large-number-no-op,numbers] diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index c306b15ef3..22aff36d67 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -123,6 +123,7 @@ Module Test6. Export Scopes. Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). End Notations. + Set Printing Coercions. Check let v := 0%wnat in v : wnat. Check wrap O. Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) |