From 3a501aec80ea400216f833cf2f30977f4ff826a3 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 18 Mar 2006 15:33:09 +0000
Subject: MAJ documentation en syntaxe v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8647 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/entries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index c31d8f74a..8bb616d8b 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -32,9 +32,9 @@ type local_entry =
 
 (* Assume the following definition in concrete syntax:
 \begin{verbatim}
-Inductive I1 [x1:X1;...;xn:Xn] : A1 := c11 : T11 | ... | c1n1 : T1n1
+Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
 ...
-with  Ip [x1:X1;...;xn:Xn] : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
+with      Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
 \end{verbatim}
 then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
 [mind_entry_arity] is [Ai], defined in context [[[x1:X1;...;xn:Xn]];
-- 
cgit v1.2.3