diff options
| -rw-r--r-- | pretyping/constr_matching.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4198.v | 24 |
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. |