diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1740.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1740.v | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v deleted file mode 100644 index ec4a7a6b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1740.v +++ /dev/null @@ -1,23 +0,0 @@ -(* Check that expansion of alias in pattern-matching compilation is no - longer dependent of whether the pattern-matching problem occurs in a - typed context or at toplevel (solved from revision 10883) *) - -Definition f := - fun n m : nat => - match n, m with - | O, _ => O - | n, O => n - | _, _ => O - end. - -Goal f = - fun n m : nat => - match n, m with - | O, _ => O - | n, O => n - | _, _ => O - end. - unfold f. - reflexivity. -Qed. - |