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 +++++++
 theories/micromega/Lia.v           | 5 ++++-
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_12907.v

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.
diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v
index b2c5884ed7..ef2f139133 100644
--- a/theories/micromega/Lia.v
+++ b/theories/micromega/Lia.v
@@ -20,7 +20,10 @@ Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
 Ltac zchecker :=
-  intros ?__wit ?__varmap ?__ff ;
+  let __wit := fresh "__wit" in
+  let __varmap := fresh "__varmap" in
+  let __ff := fresh "__ff" in
+  intros __wit __varmap __ff ;
   exact (ZTautoChecker_sound __ff __wit
                                 (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true)
                                 (@find Z Z0 __varmap)).
-- 
cgit v1.2.3