diff options
| author | Hugo Herbelin | 2014-09-02 11:37:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-02 19:28:49 +0200 |
| commit | a50aecc7a56b7b7b1c676009f1936599366eb4ba (patch) | |
| tree | 33e55e7e539cf9245fc4dcba8d860cab95e26e0f /test-suite | |
| parent | 595de46fe3de117129395157dfad28548dc0a157 (diff) | |
Another fix than 19a7a5789c to avoid descend_in_conjunction to use
fresh names interferring with names later generated in intropatterns
(as introduced in 72498d6d68ac which passed "clenv_refine_in continued
by pattern introduction" to descend_in_conjunction while only a pure
clenv_refine was passed before). The 72498d6d68ac version was
generating fresh names in the wrong order (morally-private names for
descend_in_conjunction before user-level names in clenv_refine_in).
The 19a7a5789c fix was introducing expressions not handled by the
refine from logic.ml.
In particular, this fixes RelationAlgebra.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/apply.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 48db9c41cf..7f1a8f5d45 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -489,3 +489,10 @@ split. exact H. (* Check that generated names are H and H0 *) exact H0. Qed. + +(* This failed at some time in between 18 August 2014 and 2 September 2014 *) + +Goal forall A B C: Prop, (True -> A -> B /\ C) -> A -> B. +intros * H. +apply H. +Abort. |