diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index e33d2259d3..b1becba3f5 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -157,8 +157,8 @@ More precisely the language of the {\em Calculus of Inductive occurs in $U$, $\forall~x:T,U$ reads as {\it ``for all x of type T, U''}. As $U$ depends on $x$, one says that $\forall~x:T,U$ is a {\em dependent product}. If $x$ does not occur in $U$ then - $\forall~x:T,U$ reads as {\it ``if T then U''}. A non dependent - product can be written: $T \rightarrow U$. + $\forall~x:T,U$ reads as {\it ``if T then U''}. A {\em non dependent + product} can be written: $T \rightarrow U$. \item if $x$ is a variable and $T$, $u$ are terms then $\lb x:T \mto u$ ($\kw{fun}~x:T~ {\tt =>}~ u$ in \Coq{} concrete syntax) is a term. This is a notation for the $\lambda$-abstraction of diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index f631c3717c..0e758bcab6 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -468,8 +468,8 @@ proposition $B$ or the functional dependent product from $A$ to $B$ (a construction usually written $\Pi_{x:A}.B$ in set theory). Non dependent product types have a special notation: ``$A$ {\tt ->} -$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The non dependent -product is used both to denote the propositional implication and +$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The {\em non dependent +product} is used both to denote the propositional implication and function types. \subsection{Applications |