diff options
Diffstat (limited to 'doc/Cases.tex')
| -rw-r--r-- | doc/Cases.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/Cases.tex b/doc/Cases.tex index 11e20d1101..9fcd8430c7 100644 --- a/doc/Cases.tex +++ b/doc/Cases.tex @@ -438,7 +438,7 @@ In all the previous examples the elimination predicate does not depend on the object(s) matched. But it may depend and the typical case is when we write a proof by induction or a function that yields an object of dependent type. An example of proof using \texttt{Cases} in -given in section \ref{Refine-example} +given in section \ref{refine-example} For example, we can write the function \texttt{buildlist} that given a natural number @@ -493,7 +493,7 @@ elimination predicate ${\cal P}$ should be of the form: $[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$ The user can also use \texttt{Cases} in combination with the tactic -\texttt{Refine} (see section \ref{Refine}) to build incomplete proofs +\texttt{refine} (see section \ref{refine}) to build incomplete proofs beginning with a \texttt{Cases} construction. \asection{Pattern-matching on inductive objects involving local |