From c80601d8890fd3131db0560db9fa0c18a44dd548 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 13 May 2008 14:44:23 +0000
Subject: - Fix bug related to indices of fixpoints. - Add a typeclasses_eauto
 which uses only the typeclass_instances   database. - Set obligations as
 transparent by default to avoid the   common problem with ill-formed
 recursive defs due to opaque   obligations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10925 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 5fe218fa50..0f6a5cbf6c 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -230,8 +230,8 @@ tactic is replaced by the default one if not specified.
   Shows the term that will be fed to
   the kernel once the obligations are solved. Useful for debugging.
 \item {\tt Set Transparent Obligations}\comindex{Set Transparent Obligations}
-  Force all obligations to be declared as transparent, otherwise let the
-  system infer which obligations can be declared opaque.
+  Control whether all obligations should be declared as transparent (the
+  default), or if the system should infer which obligations can be declared opaque. 
 \end{itemize}
 
 The module {\tt Coq.Program.Tactics} defines the default tactic for solving
-- 
cgit v1.2.3