From 8aebd0c751db55c0301518d8ed55b8ac7bccae27 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 May 2015 11:31:16 +0200
Subject: Turning "Set Regular Subst Tactic" on by default (for 8.6).

---
 doc/refman/RefMan-tac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index be82eaa018..e2827d6bf7 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2841,7 +2841,7 @@ Additionally, it prevents a local definition such as {\tt \ident :=
 configurations containing hypotheses of the form {\tt {\ident} = $u$},
 or {\tt $u'$ = \ident} with $u'$ not a variable.
 
-The option is off by default.
+The option is on by default.
 
 \end{Variants}
 
-- 
cgit v1.2.3