1 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
new file mode 100644
index 00000000..f85a6026
--- /dev/null
+++ b/test-suite/bugs/closed/4198.v
@@ -0,0 +1,37 @@
+(* Check that the subterms of the predicate of a match are taken into account *)
+
+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.
+
+(* This second example comes from CFGV where inspecting subterms of a
+   match is expecting to inspect first the term to match (even though
+   it would certainly be better to provide a "match x with _ end"
+   construct for generically matching a "match") *)
+
+Ltac find_head_of_head_match T :=
+  match T with context [?E] => 
+    match T with  
+    | E => fail 1 
+    | _ => constr:(E) 
+    end 
+  end.
+
+Ltac mydestruct :=
+  match goal with 
+  | |- ?T1 = _ => let E := find_head_of_head_match T1 in destruct E
+  end.
+
+Goal forall x, match x with 0 => 0 | _ => 0 end = 0.
+intros.
+mydestruct.