diff options
| author | barras | 2004-01-14 16:52:06 +0000 |
|---|---|---|
| committer | barras | 2004-01-14 16:52:06 +0000 |
| commit | e92027584f4134f4fa89a77a752bf28aedd9c44a (patch) | |
| tree | 0eefd0cf15a2f05fed2f49bf8b1ff26796fdf834 /doc/RefMan-modr.tex | |
| parent | 4ba765fe88d88e5765d6058b7d366e03318b789a (diff) | |
ajout d'une passe de latex our avoir un index correct
+ quelques petites retouches sur la doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8476 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan-modr.tex')
| -rw-r--r-- | doc/RefMan-modr.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/RefMan-modr.tex b/doc/RefMan-modr.tex index 66895f204f..e7c8614c86 100644 --- a/doc/RefMan-modr.tex +++ b/doc/RefMan-modr.tex @@ -273,9 +273,9 @@ Specification subtyping rules: \inference{% \frac{ \WTECONV{}{\Gamma_P}{\Gamma_P'}% - ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}% - ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}% - ~~~~~~~~\WTECONV{}{p}{p'} + ~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}% + ~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}% + ~~~~~~\WTECONV{}{p}{p'} }{ \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}% {\Indp{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}{p'}} |