diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2017.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2017.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v index 948cea3e..df666148 100644 --- a/test-suite/bugs/closed/shouldsucceed/2017.v +++ b/test-suite/bugs/closed/shouldsucceed/2017.v @@ -8,8 +8,8 @@ Set Implicit Arguments. Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool. Variable H : exists x : bool, True. - + Definition coef := match Some true with - Some _ => @choose _ H |_ => true -end . + Some _ => @choose _ H |_ => true +end . |