diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-03 01:38:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-08 21:15:33 +0100 |
| commit | 67091e1d155be19333c5e5bd2cc306792ca630d3 (patch) | |
| tree | 04d89c833d37447ee2a02852fb887aedac1edc81 /test-suite/bugs | |
| parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
[compat] Remove "Refolding Reduction" option.
Following up on #6791, we remove support refolding in reduction.
We also update a test case that was not properly understood, see the
discussion in #6895.
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/opened/3424.v (renamed from test-suite/bugs/closed/3424.v) | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/opened/3424.v index ee8cabf17..d1c5bb68f 100644 --- a/test-suite/bugs/closed/3424.v +++ b/test-suite/bugs/opened/3424.v @@ -13,12 +13,12 @@ Notation "0" := (trunc_S minus_one) : trunc_scope. Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. Notation IsHProp := (IsTrunc minus_one). Notation IsHSet := (IsTrunc 0). -Set Refolding Reduction. Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }. Proof. intros. eexists. (* exact (H' a b). *) (* Undo. *) -apply (H' a b). +Fail apply (H' a b). +exact (H' a b). Qed. |