diff options
| author | Jasper Hugunin | 2020-09-10 13:32:43 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-10 13:39:06 -0700 |
| commit | 172dbc86f39d79bc5323b95c2c2efa97e6a54919 (patch) | |
| tree | 99513471043f48b55dce07b92dfd20da48357d7b /test-suite | |
| parent | cdfe69d6da6b32338ba74c9f599c74389089c9dd (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_13003.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |