petits bug dans chapitre des modules

liens vers proofgeneral


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8483 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 9 insertions, 9 deletions

diff --git a/doc/RefMan-modr.tex b/doc/RefMan-modr.tex
index e7c8614c8..e08c7c401 100644
--- a/doc/RefMan-modr.tex
+++ b/doc/RefMan-modr.tex
@@ -155,7 +155,7 @@ meaning:
   follows:
   \begin{itemize}
   \item $\Def{}{c}{U}{t}/p ~=~ \Def{}{c}{U}{t}$
-  \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{U}{p.c}$
+  \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{p.c}{U}$
   \item $\ModS{X}{T}/p ~=~ \ModSEq{X}{T/p.X}{p.X}$
   \item $\ModSEq{X}{T}{p'}/p ~=~ \ModSEq{X}{T/p}{p'}$
   \item $\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$
@@ -228,7 +228,7 @@ Specification subtyping rules:
   \frac{
     \WTELECONV{}{U_1}{U_2}
   }{
-    \WSE{\Def{}{c}{U_1}{t}}{\Assum{}{c}{U_2}}
+    \WSE{\Def{}{c}{t}{U_1}}{\Assum{}{c}{U_2}}
   }
 }
 \item[ASSUM-DEF]
@@ -236,7 +236,7 @@ Specification subtyping rules:
   \frac{
     \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{c}{t_2}
   }{
-    \WSE{\Assum{}{c}{U_1}}{\Def{}{c}{U_2}{t_2}}
+    \WSE{\Assum{}{c}{U_1}}{\Def{}{c}{t_2}{U_2}}
   }
 }
 \item[DEF-DEF]
@@ -244,7 +244,7 @@ Specification subtyping rules:
   \frac{
     \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
   }{
-    \WSE{\Def{}{c}{U_1}{t_1}}{\Def{}{c}{U_2}{t_2}}
+    \WSE{\Def{}{c}{t_1}{U_1}}{\Def{}{c}{t_2}{U_2}}
   }
 }
 \item[IND-IND]
@@ -406,7 +406,7 @@ Component access rules
 \\
 \inference{%
   \frac{
-    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{U}{t};\dots}}
+    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{t}{U};\dots}}
   }{
     \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
@@ -416,7 +416,7 @@ Notice that the following rule extends the delta rule defined in
 section~\ref{delta}
 \inference{%
   \frac{
-    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{U}{t};\dots}}
+    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{t}{U};\dots}}
   }{
     \WTEGRED{p.c}{\triangleright_\delta}{\subst{t}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
@@ -496,7 +496,7 @@ $\lab{\Spec_1;\dots;\Spec_n}=\lab{\Spec_1}\cup\dots;\cup\lab{\Spec_n}$
 where $\lab{\Spec}$ is defined as follows:
 \begin{itemize}
 \item $\lab{\Assum{\Gamma}{c}{U}}=\{c\}$,
-\item $\lab{\Def{\Gamma}{c}{U}{t}}=\{c\}$,
+\item $\lab{\Def{\Gamma}{c}{t}{U}}=\{c\}$,
 \item
   $\lab{\Ind{\Gamma}{\Gamma_P}{\Gamma_C}{\Gamma_I}}=\dom{\Gamma_C}\cup\dom{\Gamma_I}$,
 \item $\lab{\ModS{m}{T}}=\{m\}$,
diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex
index 9a598b193..956d7568c 100755
--- a/doc/RefMan-uti.tex
+++ b/doc/RefMan-uti.tex
@@ -254,7 +254,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
 files. 
 
 Proof General is developped and distributed independently of the
-system \Coq. It is freely available at \verb!www.proofgeneral.org!.
+system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
 
 
 \section{Module specification}\label{gallina}\index{Gallina@{\tt gallina}}
diff --git a/doc/macros.tex b/doc/macros.tex
index 7417145eb..d129d9d10 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -399,7 +399,7 @@
 \newcommand{\ModType}[2]{{\sf ModType}({#1}:={#2})}
 \newcommand{\ModS}[2]{{\sf ModS}({#1}:{#2})}
 \newcommand{\ModSEq}[3]{{\sf ModSEq}({#1}:{#2}=={#3})}
-\newcommand{\functor}[3]{\ensuremath{{\sf Functor}[#1:#2]\;#3}}
+\newcommand{\functor}[3]{\ensuremath{{\sf Functor}(#1:#2)\;#3}}
 \newcommand{\funsig}[3]{\ensuremath{{\sf Funsig}(#1:#2)\;#3}}
 \newcommand{\sig}[1]{\ensuremath{{\sf Sig}~#1~{\sf End}}}
 \newcommand{\struct}[1]{\ensuremath{{\sf Struct}~#1~{\sf End}}}