From e08f20e13cdd2ba23ea7c1e0e1824e585df6e501 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 31 Jan 2007 09:48:48 +0000
Subject: Fix typo.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9565 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/Program.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman/Program.tex')

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index ea694f61d2..2025164f2e 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -174,7 +174,7 @@ The following commands are available to manipulate obligations:
   each obligation using the given tactic.
 \item {\tt Admit Obligations [of \ident]} Admits all
   obligations (does not work with structurally recursive programs).
-\item {\tt Obligations Tactic := \expr} Sets the default obligation
+\item {\tt Obligations Tactic := \tacexpr} Sets the default obligation
   solving tactic applied to all obligations.
 \end{itemize}
   
-- 
cgit v1.2.3