From 179a23ad345c6d0753bbb1771fc01f402dc1cb33 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 26 Aug 2020 07:38:53 -0700
Subject: Modify lia to work with -mangle-names

We used to be refreshing the names for intros but not using the
refreshed names. The same pattern of `intro_using` (which is what
`intros ?name` effectively is) messing things up as in coq/coq#12881.
---
 test-suite/bugs/closed/bug_12907.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12907.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_12907.v b/test-suite/bugs/closed/bug_12907.v
new file mode 100644
index 0000000000..4cd79cc1af
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12907.v
@@ -0,0 +1,7 @@
+From Coq Require Export Lia.
+Set Mangle Names.
+Lemma test (n : nat) : n <= 10 -> n <= 20.
+Proof. lia. Qed.
+
+Lemma test2 : 0 < 1.
+Proof. lia. Qed.
-- 
cgit v1.2.3