1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v
new file mode 100644
index 00000000..d9ce546a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1740.v
@@ -0,0 +1,23 @@
+(* 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.
+