diff options
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} |