From 7ea0db435910c2db2a9ae4cadfd54f49f3640b62 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 18 Jan 2021 21:22:52 -0800
Subject: Remove the Hide Obligations flag

---
 doc/sphinx/addendum/program.rst | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'doc/sphinx/addendum/program.rst')

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 2b24ced8a1..8f2b51ccce 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -320,14 +320,6 @@ optional tactic is replaced by the default one if not specified.
    (the default), or if the system should infer which obligations can be
    declared opaque.
 
-.. flag:: Hide Obligations
-
-   .. deprecated:: 8.12
-
-   Controls whether obligations appearing in the
-   term should be hidden as implicit arguments of the special
-   constant ``Program.Tactics.obligation``.
-
 The module :g:`Coq.Program.Tactics` defines the default tactic for solving
 obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also
 adds some useful notations, as documented in the file itself.
-- 
cgit v1.2.3