diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-12-05 12:35:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-27 17:23:17 +0200 |
| commit | 9839375100365ea3bd28bfc2efdb701db7d83adb (patch) | |
| tree | 0e26b4109b809ce587852eedb3682f8d35cb5e32 /test-suite | |
| parent | e2a8edaf595827af82be67a90c0c5b22c987abe5 (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.v | 10 |
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. |