From eb905490e4f02ab4a626b32ad9b83cc44e94d4c0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Nov 2003 14:14:53 +0000
Subject: 'as' avant 'using' dans 'destruct'

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

(limited to 'doc')

diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index dfefabaf54..21c95d3264 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -419,12 +419,12 @@ $$
 \nlsep \TERM{lapply}~\tacconstr
 %%
 \nlsep \TERM{simple_induction}~\NT{quantified-hyp}
-\nlsep \TERM{induction}~\NT{induction-arg}~\OPT{\NT{eliminator}}
-       ~\OPT{\NT{with-names}}
+\nlsep \TERM{induction}~\NT{induction-arg}~\OPT{\NT{with-names}}
+       ~\OPT{\NT{eliminator}}
 \nlsep \TERM{double}~\TERM{induction}~\NT{quantified-hyp}~\NT{quantified-hyp}
 \nlsep \TERM{simple_destruct}~\NT{quantified-hyp}
-\nlsep \TERM{destruct}~\NT{induction-arg}~\OPT{\NT{eliminator}}
-       ~\OPT{\NT{with-names}}
+\nlsep \TERM{destruct}~\NT{induction-arg}~\OPT{\NT{with-names}}
+       ~\OPT{\NT{eliminator}}
 \nlsep \TERM{decompose}~\TERM{record}~\tacconstr
 \nlsep \TERM{decompose}~\TERM{sum}~\tacconstr
 \nlsep \TERM{decompose}~\TERM{[}~\PLUS{\NT{reference}}~\TERM{]}
-- 
cgit v1.2.3