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/opened | |
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/opened')
-rw-r--r-- | test-suite/bugs/opened/3424.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3424.v b/test-suite/bugs/opened/3424.v new file mode 100644 index 000000000..d1c5bb68f --- /dev/null +++ b/test-suite/bugs/opened/3424.v @@ -0,0 +1,24 @@ +Set Universe Polymorphism. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }. +Inductive trunc_index : Type := minus_two | trunc_S (x : trunc_index). +Bind Scope trunc_scope with trunc_index. +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | minus_two => Contr_internal A + | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) + end. +Notation minus_one:=(trunc_S minus_two). +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). +Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }. +Proof. +intros. +eexists. +(* exact (H' a b). *) +(* Undo. *) +Fail apply (H' a b). +exact (H' a b). +Qed. |