diff options
| author | Vincent Laporte | 2020-08-11 10:05:11 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2020-08-11 10:05:11 +0200 |
| commit | 83ca3cb2e715b66e04987048ed6e4af1f7400d89 (patch) | |
| tree | d72605fc24eb7ba1287f11d7123fe8e3fe5bd6c6 /test-suite | |
| parent | d5a8bdc8f67b691dd39a27a9fe07a026d998fda3 (diff) | |
| parent | 4da8f114155d2abb31ce8a45a2f17f21f7d97a0e (diff) | |
Merge PR #12814: [zify] fix for bug#12791
Reviewed-by: vbgl
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/micromega/bug_12791.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/micromega/bug_12791.v b/test-suite/micromega/bug_12791.v new file mode 100644 index 0000000000..8aec1904a4 --- /dev/null +++ b/test-suite/micromega/bug_12791.v @@ -0,0 +1,9 @@ +Require Import Lia. + +Definition t := nat. + +Goal forall (a b: t), let c := a in b = a -> b = c. +Proof. + intros a b c H. + lia. +Qed. |