From 5f50ee87842b5741743e2f8a240e27fccb8311bd Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 5 Sep 2012 18:25:51 +0000
Subject: Obsolete syntax in documentation of Solve Obligation commands.

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

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

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index fee070fd65..5632aac42a 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -241,11 +241,11 @@ tactic is replaced by the default one if not specified.
   obligation {\tt num}.
 \item {\tt Next Obligation [of \ident]}\comindex{Next Obligation} Start the proof of the next
   unsolved obligation.
-\item {\tt Solve Obligations [of \ident] [using
+\item {\tt Solve Obligations [of \ident] [with
     \tacexpr]}\comindex{Solve Obligations}
   Tries to solve
   each obligation of \ident using the given tactic or the default one.
-\item {\tt Solve All Obligations [using \tacexpr]} Tries to solve
+\item {\tt Solve All Obligations [with \tacexpr]} Tries to solve
   each obligation of every program using the given tactic or the default
   one (useful for mutually recursive definitions).
 \item {\tt Admit Obligations [of \ident]}\comindex{Admit Obligations} 
-- 
cgit v1.2.3