diff options
| author | Pierre-Marie Pédrot | 2016-02-03 15:32:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-13 17:26:35 +0100 |
| commit | f46a5686853353f8de733ae7fbd21a3a61977bc7 (patch) | |
| tree | 0d26cb4280faa70491d83d7665466c9c1ad6d2d5 /test-suite/bugs | |
| parent | df6bb883920e3a03044d09f10b57a44a2e7c5196 (diff) | |
Do not give a name to anonymous evars anymore. See bug #4547.
The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/3068.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v index ced6d95949..79671ce930 100644 --- a/test-suite/bugs/closed/3068.v +++ b/test-suite/bugs/closed/3068.v @@ -56,7 +56,7 @@ Section Finite_nat_set. subst fs1. apply iff_refl. intros H. - eapply counted_list_equal_nth_char. + eapply (counted_list_equal_nth_char _ _ _ _ ?[def]). intros i. destruct (counted_def_nth fs1 i _ ) eqn:H0. (* This was not part of the initial bug report; this is to check that |