diff options
| author | william-lawvere | 2017-07-01 23:14:10 -0700 |
|---|---|---|
| committer | GitHub | 2017-07-01 23:14:10 -0700 |
| commit | 66b1132128481b0e3a461862518e9eaf34838e0c (patch) | |
| tree | 54a339672210eeeb02baa6b42b5af00e927cfbbd | |
| parent | 80649ebaba75838bfd28ae78822cd2c078da4b23 (diff) | |
Update RefMan-syn.tex
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index a409d61bb8..f4fb86b876 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -89,7 +89,7 @@ more than a higher level. Hence the level for disjunction must be higher than the level for conjunction. Since connectives are not tight articulation points of a text, it -is reasonable to choose levels not so far from the higher level which +is reasonable to choose levels not so far from the highest level which is 100, for example 85 for disjunction and 80 for conjunction\footnote{which are the levels effectively chosen in the current implementation of {\Coq}}. |