diff options
author | 2014-12-09 12:00:10 +0100 | |
---|---|---|
committer | 2014-12-09 12:14:41 +0100 | |
commit | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (patch) | |
tree | 52eee33926e6791b4d2ac23c04f48404057899b4 /doc/refman/RefMan-coi.tex | |
parent | 56302f63809494946adf4e805bc61d55ed9d6f14 (diff) |
refman: switch all source files to utf8
Putting utf8 everywhere helps the maintainance of the online refman.
And anyway, this is the way to go. We should also chase and migrate
the few remaining iso-latin-1 files elsewhere in the sources.
Diffstat (limited to 'doc/refman/RefMan-coi.tex')
-rw-r--r-- | doc/refman/RefMan-coi.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex index 4ef5818aa..dac3c60bd 100644 --- a/doc/refman/RefMan-coi.tex +++ b/doc/refman/RefMan-coi.tex @@ -184,7 +184,7 @@ Eval compute in (tl nat (from 0)). $(\from\;n)\equiv(\cons\;\nat\;n\;(\from \; (\S\;n)))$ does not hold as definitional one. Nevertheless, it can be proved as a propositional equality, in the sense of Leibniz's equality. -The version {\it à la Leibniz} of the equality above follows from +The version {\it à la Leibniz} of the equality above follows from a general lemma stating that eliminating and then re-introducing a stream yields the same stream. \begin{coq_example} |