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.

2 files changed, 25 insertions, 1 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5098665582..a0493777a5 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -419,7 +419,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       | [] -> assert false
       | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
       in
-      let sub = (env, hd) :: (env, c1) :: subargs env lc in
+      let sub = (env, c1) :: (env, hd) :: subargs env lc in
       try_aux sub next_mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index ef991365d5..f85a60264d 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.