From a6757b089e1d268517bcba48a9fe33aa47526de2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 25 Jan 2019 00:06:32 +0100 Subject: Remove Refine Instance Mode option --- doc/sphinx/changes.rst | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'doc/sphinx/changes.rst') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5e337bcef0..cc2c43e7dd 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -486,10 +486,9 @@ Other changes in 8.10+beta1 - :cmd:`Declare Instance` now requires an instance name. - The flag :flag:`Refine Instance Mode` has been turned off by default, - meaning that :cmd:`Instance` no longer opens a proof when a body is - provided. The flag has been deprecated and will be removed in the next - version. + The flag `Refine Instance Mode` has been turned off by default, meaning that + :cmd:`Instance` no longer opens a proof when a body is provided. The flag + has been deprecated and will be removed in the next version. (`#9270 `_, and `#9825 `_, -- cgit v1.2.3