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.
---
 theories/micromega/Lia.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'theories/micromega')

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