From 1cb9fe4d99d82260074419ac4ada5d6058ae165c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 15 Feb 2007 18:30:14 +0000
Subject: Réintroduction de l'entrée "integer" dans ltac (apparemment disparue
 lors du passage de l'ancienne à la nouvelle syntaxe)

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 79a33712dd..41f38046e0 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -138,6 +138,7 @@ is understood as
 {\atom} & ::= &
            {\qualid} \\
 & | & ()\\
+& | & {\integer}\\
 & | & {\tt (} {\tacexpr} {\tt )}\\
 \\
 {\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\term} ~|~ {\integer} \\
-- 
cgit v1.2.3