From e02120ed6580733db2276f0c11b4f432ea670ee3 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 12 Sep 2020 20:54:22 -0700
Subject: Convert rewriting and proof-mode chapters to prodn

---
 doc/sphinx/addendum/program.rst | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 104f84a253..2b24ced8a1 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -161,7 +161,7 @@ Program Definition
 A :cmd:`Definition` command with the :attr:`program` attribute types
 the value term in Russell and generates proof
 obligations. Once solved using the commands shown below, it binds the
-final Coq term to the name :n:`@ident` in the environment.
+final Coq term to the name :n:`@ident` in the global environment.
 
 :n:`Program Definition @ident : @type := @term`
 
@@ -268,7 +268,6 @@ obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
 .. cmd:: Obligation Tactic := @ltac_expr
-   :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
    automatically, whether to solve them or when starting to prove one,
-- 
cgit v1.2.3