diff options
| author |  William Lawvere <mundungus.corleone@gmail.com> | 2017-07-01 22:08:44 -0700 |
|---|---|---|
| committer | William Lawvere <mundungus.corleone@gmail.com> | 2017-07-01 22:08:44 -0700 |
| commit | c2942e642ee6f83cc997f9a2510cdb7446a65cb4 (patch) | |
| tree | a57b95497f1389db751b7b04e42e3e70540d05c6 /doc | |
| parent | ce22b7634aa33afb4f5ee09c2b8c10bf76637234 (diff) | |
RefMan-gal: improve grammar
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 3814e4403..71977d3e9 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -3,7 +3,7 @@ \label{BNF-syntax} % Used referred to as a chapter label This chapter describes \gallina, the specification language of {\Coq}. -It allows developing mathematical theories and to prove specifications +It allows developing mathematical theories and proofs of specifications of programs. The theories are built from axioms, hypotheses, parameters, lemmas, theorems and definitions of constants, functions, predicates and sets. The syntax of logical objects involved in |