diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-19 14:16:34 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-19 14:16:34 +0000 |
| commit | fc5df964ec52be014bfd16ef6d8f56ec1f153834 (patch) | |
| tree | 1c625d026a0764a954fc1c5eb90d4c260b60ae44 | |
| parent | 0848c14357f23c6e9ffdf5cacc02cbc30f530d31 (diff) | |
Fix typo in omega doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11604 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/Omega.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex index bbf17f630..b9e899ce8 100644 --- a/doc/refman/Omega.tex +++ b/doc/refman/Omega.tex @@ -16,7 +16,7 @@ may use any hypothesis of the current proof session to solve the goal. Multiplication is handled by {\tt omega} but only goals where at least one of the two multiplicands of products is a constant are -solvable. This is the restriction meaned by ``Presburger arithmetic''. +solvable. This is the restriction meant by ``Presburger arithmetic''. If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. |