diff options
author | 2005-05-05 21:14:38 +0000 | |
---|---|---|
committer | 2005-05-05 21:14:38 +0000 | |
commit | aceda714576e1cbaa12dbf1f12507c8a625934ef (patch) | |
tree | 0417c57d704bb3a826df4d00f6c81c3339c656a6 | |
parent | c0241d44c104f11ae7f9c7c852b0b5852e65605d (diff) |
suite commit pr�c�dent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8601 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-x | doc/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex index 9ba5bdaf1..52745b7a9 100755 --- a/doc/RefMan-cic.tex +++ b/doc/RefMan-cic.tex @@ -830,7 +830,7 @@ Inductive exSet (P:Set->Prop) : Set It is possible to declare the same inductive definition in the universe \Type. The \texttt{exType} inductive definition has type $(\Type_i \ra\Prop)\ra -\Type_j$ with the constraint that the argument $X$ of \texttt{exT\_intro} has type $\Type_k$ with $k<j$ and $k\leq i$. +\Type_j$ with the constraint that the parameter \texttt{X} of \texttt{exT\_intro} has type $\Type_k$ with $k<j$ and $k\leq i$. \begin{coq_example*} Inductive exType (P:Type->Prop) : Type := exT_intro : forall X:Type, P X -> exType P. |