diff options
| author | Hugo Herbelin | 2019-11-18 16:27:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-08 18:23:53 +0100 |
| commit | d696eb98189eccdc2f6adb851e54af37e7f8d83b (patch) | |
| tree | d7ab5a496defc1004cb851cceb46664d34ca0e46 /test-suite | |
| parent | 756d2f4db5eae51c8c01a40550b8c4553bd30f53 (diff) | |
When printing term together with its type, use info that term is in context.
This governs the printing of the explicitation of implicit arguments
and the removal of coercions.
E.g., "Check coe foo." where coe is a coercion with codomain B will show:
foo
: B
instead of
coe foo
: B
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 *) |