From 2b3bd349914a759b270cea48a7ec32c9320f1792 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 22:41:07 -0400
Subject: [obligations] Deprecated flag cleanup

We deprecate `Hide Obligations` and remove `Shrink Obligations`
[deprecated since 8.7]
---
 test-suite/success/shrink_obligations.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/shrink_obligations.v b/test-suite/success/shrink_obligations.v
index 676b97878f..032fcaac6d 100644
--- a/test-suite/success/shrink_obligations.v
+++ b/test-suite/success/shrink_obligations.v
@@ -2,8 +2,6 @@ Require Program.
 
 Obligation Tactic := idtac.
 
-Set Shrink Obligations.
-
 Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit :=
 let bar : {r | n < r} := _ in
 let qux : {r | p < r} := _ in
-- 
cgit v1.2.3