diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:00:10 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:14:41 +0100 |
commit | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (patch) | |
tree | 52eee33926e6791b4d2ac23c04f48404057899b4 /doc/refman/RefMan-lib.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-lib.tex')
-rw-r--r-- | doc/refman/RefMan-lib.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 5f1e11c47..49382f3e2 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -485,7 +485,7 @@ Inductive sumor (A:Set) (B:Prop) : Set := | inright (_:B). \end{coq_example*} -We may define variants of the axiom of choice, like in Martin-Löf's +We may define variants of the axiom of choice, like in Martin-Löf's Intuitionistic Type Theory. \ttindex{Choice} \ttindex{Choice2} |