diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /test-suite/bugs/closed/4198.v | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/bugs/closed/4198.v')
-rw-r--r-- | test-suite/bugs/closed/4198.v | 37 |
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. |