diff options
| author | coqbot-app[bot] | 2021-01-26 11:08:28 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-26 11:08:28 +0000 |
| commit | 1a84bed789697ff9b4f5c70dec3c732cdbbdbce0 (patch) | |
| tree | 85cbefe72ebbeaa9b3d6c1c27545864f96faa245 /doc/sphinx/addendum | |
| parent | 14051337936db1f56dc052a6e54e5b606552141b (diff) | |
| parent | 7ea0db435910c2db2a9ae4cadfd54f49f3640b62 (diff) | |
Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 8 |
1 files changed, 0 insertions, 8 deletions
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. |