diff options
Diffstat (limited to 'doc/RefMan-uti.tex')
| -rwxr-xr-x | doc/RefMan-uti.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex index ccba33b48..b812a3042 100755 --- a/doc/RefMan-uti.tex +++ b/doc/RefMan-uti.tex @@ -270,7 +270,7 @@ Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its specification (inductive types declarations, definitions, type of lemmas and theorems), removing the proofs parts of the file. The \Coq\ file {\em file}{\tt.v} gives birth to the specification file -{\em file}{\tt.g} (where the suffix {\tt.g} stands for {\sf Gallina}). +{\em file}{\tt.g} (where the suffix {\tt.g} stands for \gallina). See the man page of {\tt gallina} for more details and options. |