diff options
| author | William Lawvere | 2017-07-01 22:08:44 -0700 |
|---|---|---|
| committer | William Lawvere | 2017-07-01 22:08:44 -0700 |
| commit | c2942e642ee6f83cc997f9a2510cdb7446a65cb4 (patch) | |
| tree | a57b95497f1389db751b7b04e42e3e70540d05c6 | |
| parent | ce22b7634aa33afb4f5ee09c2b8c10bf76637234 (diff) | |
RefMan-gal: improve grammar
| -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 3814e4403a..71977d3e9d 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 |