From 67091e1d155be19333c5e5bd2cc306792ca630d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 3 Mar 2018 01:38:19 +0100
Subject: [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.
---
 test-suite/bugs/closed/3424.v | 24 ------------------------
 test-suite/bugs/opened/3424.v | 24 ++++++++++++++++++++++++
 2 files changed, 24 insertions(+), 24 deletions(-)
 delete mode 100644 test-suite/bugs/closed/3424.v
 create mode 100644 test-suite/bugs/opened/3424.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/closed/3424.v
deleted file mode 100644
index ee8cabf171..0000000000
--- a/test-suite/bugs/closed/3424.v
+++ /dev/null
@@ -1,24 +0,0 @@
-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).
-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).
-Qed.
diff --git a/test-suite/bugs/opened/3424.v b/test-suite/bugs/opened/3424.v
new file mode 100644
index 0000000000..d1c5bb68f9
--- /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.
-- 
cgit v1.2.3