Better fixing #4198 such that the term to match is looked for before

the predicate, thus respecting the visual left-to-right top-down order
(see a45bd5981092).

This fixes CFGV.

1 files changed, 24 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index ef991365d..f85a60264 100644
--- a/test-suite/bugs/closed/4198.v
+++ b/test-suite/bugs/closed/4198.v
@@ -1,3 +1,5 @@
+(* 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'),
@@ -11,3 +13,25 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
   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.