diff options
Diffstat (limited to 'test-suite/success/extraction.v')
| -rw-r--r-- | test-suite/success/extraction.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 0b3060d5..74d87ffa 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -84,7 +84,7 @@ Extraction test12. (* type test12 = (__ -> __ -> __) -> __ *) -Definition test13 := match left True I with +Definition test13 := match @left True True I with | left x => 1 | right x => 0 end. |