From 43869b4e05824244e666c60e0b740a80e8b09d0c Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 28 Jun 2016 12:37:00 -0400
Subject: no-refold patch

Add a boolean for refolding during reduction, and an option
that is off by default in 8.6, to turn refolding on in all reduction
functions, as in 8.5.
---
 test-suite/bugs/closed/3424.v | 1 +
 test-suite/output/inference.v | 1 +
 2 files changed, 2 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/closed/3424.v
index f9b2c38611..ee8cabf171 100644
--- a/test-suite/bugs/closed/3424.v
+++ b/test-suite/bugs/closed/3424.v
@@ -13,6 +13,7 @@ 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.
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index cd9a4a12b2..1825db1676 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -14,6 +14,7 @@ Definition P (e:option L) :=
 Print P.
 
 (* Check that plus is folded even if reduction is involved *)
+Set Refolding Reduction.
 Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 
 
-- 
cgit v1.2.3