diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1740.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1740.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v index d9ce546a..ec4a7a6b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1740.v +++ b/test-suite/bugs/closed/shouldsucceed/1740.v @@ -17,7 +17,7 @@ Goal f = | n, O => n | _, _ => O end. - unfold f. + unfold f. reflexivity. Qed. |