diff options
| author | Hugo Herbelin | 2019-11-18 15:29:18 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-17 22:11:14 +0100 |
| commit | fd40254f02f4640bbfcad5a010a8a0062989eeb9 (patch) | |
| tree | 182fac53264baae7454ad611fe3212790b6ef306 /test-suite | |
| parent | c51323a3cf1f4bb4c1ec170e3a1acfc6f5b1696b (diff) | |
Mini-improvements in when to skip coercions or explicitly print implicit args.
If a return type is given to a match/if/let, then we are in context
(and thus may skip coercions or not make explicit those implicit
arguments inferable from context). Note that the notion of "inferable
from context" remains anyway an approximation in the case of implicit
arguments.
The body of a fix/cofix is also in context.
Also fixed an inconsistency with parsing in the scope used to print
the body of a fix.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Implicit.out | 5 | ||||
| -rw-r--r-- | test-suite/output/Implicit.v | 10 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 5f22eb5d7c..d081089652 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -12,3 +12,8 @@ map id' (1 :: nil) : list nat map (id'' (A:=nat)) (1 :: nil) : list nat +fix f (x : nat) : option nat := match x with + | 0 => None + | S _ => x + end + : nat -> option nat diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 306532c0df..a7c4399e38 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -51,3 +51,13 @@ Definition id'' (A:Type) (x:A) := x. Check map (@id'' nat) (1::nil). +Module MatchBranchesInContext. + +Set Implicit Arguments. +Set Contextual Implicit. + +Inductive option A := None | Some (a:A). +Coercion some_nat := @Some nat. +Check fix f x := match x with 0 => None | n => some_nat n end. + +End MatchBranchesInContext. |