From 3d2cf9fea0aec4ae839f70acd896958772b4caaf Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 21 Apr 2015 17:12:29 +0200 Subject: Test for #4198 (appcontext in return clause of match). --- test-suite/bugs/closed/4198.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test-suite/bugs/closed/4198.v (limited to 'test-suite/bugs/closed/4198.v') diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v new file mode 100644 index 000000000..ef991365d --- /dev/null +++ b/test-suite/bugs/closed/4198.v @@ -0,0 +1,13 @@ +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. -- cgit v1.2.3