From 4da8f114155d2abb31ce8a45a2f17f21f7d97a0e Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 10 Aug 2020 15:31:58 +0200
Subject: [zify] fix for bug#12791

The elimination of let bindings is performing a convertibility check in
order to deal with type aliases.
---
 test-suite/micromega/bug_12791.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/micromega/bug_12791.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3