diff options
| author | Enrico Tassi | 2015-02-12 22:33:22 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-12 22:34:07 +0100 |
| commit | 7d06e602bea9e7a2c98e1c6badab3a667714b5c8 (patch) | |
| tree | 62409528606ad9df107cf28260f8da8a7fd5b6ba /doc | |
| parent | 154bb6a5134c35caea187b83334c098dbadb4e48 (diff) | |
Fix typos about .vio files (thanks Arthur for spotting them)
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 71eb0108d3..11b4f26145 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1059,7 +1059,7 @@ Please note that the questions described here have been subject to redesign in Coq v8.5. Former versions of Coq use the same terminology to describe slightly different things. -Compiled files (\texttt{.vo} and \texttt{.vi}) store sub-libraries. In +Compiled files (\texttt{.vo} and \texttt{.vio}) store sub-libraries. In order to refer to them inside {\Coq}, a translation from file-system names to {\Coq} names is needed. In this translation, names in the file system are called {\em physical} paths while {\Coq} names are |