aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-12-05 12:35:01 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-27 17:23:17 +0200
commit9839375100365ea3bd28bfc2efdb701db7d83adb (patch)
tree0e26b4109b809ce587852eedb3682f8d35cb5e32 /test-suite
parente2a8edaf595827af82be67a90c0c5b22c987abe5 (diff)
Test surgical use of beta-iota in the type of variables coming from
pattern-matching for refine.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/5219.v10
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5219.v b/test-suite/bugs/closed/5219.v
new file mode 100644
index 000000000..f7cec1a0c
--- /dev/null
+++ b/test-suite/bugs/closed/5219.v
@@ -0,0 +1,10 @@
+(* Test surgical use of beta-iota in the type of variables coming from
+ pattern-matching for refine *)
+
+Goal forall x : sigT (fun x => x = 1), True.
+ intro x; refine match x with
+ | existT _ x' e' => _
+ end.
+ lazymatch goal with
+ | [ H : _ = _ |- _ ] => idtac
+ end.