Test for #4198 (appcontext in return clause of match).

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
new file mode 100644
index 000000000..ef991365d
--- /dev/null
+++ b/test-suite/bugs/closed/4198.v
@@ -0,0 +1,13 @@
+Require Import List.
+Open Scope list_scope.
+Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
+       let k :=
+           (match H in (_ = y) return x = hd x y with
+              | eq_refl => eq_refl
+            end : x = x')
+       in k = k.
+  simpl.
+  intros.
+  match goal with
+    | [ |- appcontext G[@hd] ] => idtac
+  end.