From d71a32d3700980c07af2d7858147598b961607d6 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 11 Aug 2012 17:45:12 +0000
Subject: Added support for option Local (at module level) in Tactic Notation.

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

(limited to 'doc/common')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index d0512c852..1bae52617 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -168,7 +168,7 @@
 \newcommand{\flag}{\nterm{flag}}
 \newcommand{\form}{\nterm{form}}
 \newcommand{\entry}{\nterm{entry}} 
-\newcommand{\proditem}{\nterm{production\_item}}
+\newcommand{\proditem}{\nterm{prod\_item}}
 \newcommand{\taclevel}{\nterm{tactic\_level}}
 \newcommand{\tacargtype}{\nterm{tactic\_argument\_type}} 
 \newcommand{\scope}{\nterm{scope}} 
-- 
cgit v1.2.3