From 172dbc86f39d79bc5323b95c2c2efa97e6a54919 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Thu, 10 Sep 2020 13:32:43 -0700
Subject: Use fresher names in eqschemes.

The previous implementation appears to be sound when Mangle Names is
off, but it relies on two fragile assumptions, namely that
next_global_ident_away always returns different identifiers when called
with naming hints which are different after stripping all digits from
the end, and that default_id_of_sort (locally defined) never returns
"HC" or "P", or either of those followed by a string of digits.

These changes make both assumptions unnecessary.

As a side note, it seems odd that fresh is ignoring it's env parameter.
---
 test-suite/bugs/closed/bug_13003.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13003.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13003.v b/test-suite/bugs/closed/bug_13003.v
new file mode 100644
index 0000000000..570baef2ef
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13003.v
@@ -0,0 +1,9 @@
+Set Mangle Names.
+Import EqNotations.
+Lemma eq_sigT_sig_eq X P (x1 x2:X) H1 H2 :
+  forall (E1 : x1=x2), rew E1 in H1 = H2 -> existT P x1 H1 = existT P x2 H2.
+Proof.
+  intros ->.
+  intros <-.
+  reflexivity.
+Defined.
-- 
cgit v1.2.3