diff options
| author | herbelin | 2006-03-18 15:33:09 +0000 |
|---|---|---|
| committer | herbelin | 2006-03-18 15:33:09 +0000 |
| commit | 3a501aec80ea400216f833cf2f30977f4ff826a3 (patch) | |
| tree | 26f3111167b464478bb831b521b869b9a4709206 /kernel | |
| parent | 10fe13c66c704c827dc0b3ef0739a72fbc77c78d (diff) | |
MAJ documentation en syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8647 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 4 | ||||
| -rw-r--r-- | kernel/entries.mli | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index c31d8f74ab..8bb616d8b7 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]]; diff --git a/kernel/entries.mli b/kernel/entries.mli index 6f4f343bbe..2e40099b32 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -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]]; |