diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 11:40:25 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 11:40:25 +0200 |
| commit | 041b8bc806f85114bc3b54101faa84996d6ab50b (patch) | |
| tree | d6a451ddaec41ebefa9aedc60c93da67b0442f08 /test-suite/bugs/closed/3036.v | |
| parent | 83ae5e6ad95372912ba9eb9f8c52d857cdf10021 (diff) | |
Fix test-suite file for bug # 3036, the unification has _never_ succeeded,
as this would result in an ill-scoped substitution.
Diffstat (limited to 'test-suite/bugs/closed/3036.v')
| -rw-r--r-- | test-suite/bugs/closed/3036.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3036.v b/test-suite/bugs/closed/3036.v index c1ead0557..451bec9b2 100644 --- a/test-suite/bugs/closed/3036.v +++ b/test-suite/bugs/closed/3036.v @@ -165,4 +165,5 @@ Section Stack. | None => [False] end) * emp. Proof. - intros. apply himp_ex_conc_trivial. + intros. + try apply himp_ex_conc_trivial. |