diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:52:02 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:52:02 +0000 |
| commit | 0a329ae992825e98314ba4c6c4c6152d60b2bbeb (patch) | |
| tree | 68d3810338a72046f259e2ae0a44a3f316b9c0cd /doc/refman/RefMan-ext.tex | |
| parent | b2f2727670853183bfbcbafb9dc19f0f71494a7b (diff) | |
Manual fixed w.r.t. STM
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16675 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index fc511a45c..f5ad9d913 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -417,9 +417,9 @@ patterns to do the deconstruction. For example: \begin{coq_example} Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := let '((a,b), (c, d)) := x in (a,b,c,d). -Notation " x 'with' p " := (exist _ x p) (at level 20). +Notation " x 'With' p " := (exist _ x p) (at level 20). Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := - let 'x with p := t in x. + let 'x With p := t in x. \end{coq_example} When printing definitions which are written using this construct it |