diff options
| author | Gaëtan Gilbert | 2019-02-07 11:56:19 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-12 14:39:49 +0100 |
| commit | e5fb9c5cbce5e7e7e8fcb3d82c45074f9c165158 (patch) | |
| tree | c769ba01f6e235f8ec021a2531477e6eda9d6290 | |
| parent | d32a0db7b4d0775820b306badfe8072bd74cf62d (diff) | |
Fix failing coqtops in micromega.rst (the main one requires csdp)
Maybe we should still let it run but let's disable it until we install
csdp on the build server at least.
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index b076aac1ed..e56b36caad 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -124,7 +124,7 @@ and checked to be :math:`-1`. that :tacn:`omega` does not solve, such as the following so-called *omega nightmare* :cite:`TheOmegaPaper`. -.. coqtop:: in +.. coqdoc:: Goal forall x y, 27 <= 11 * x + 13 * y <= 45 -> @@ -234,7 +234,8 @@ proof by abstracting monomials by variables. To illustrate the working of the tactic, consider we wish to prove the following Coq goal: -.. coqtop:: all +.. needs csdp +.. coqdoc:: Require Import ZArith Psatz. Open Scope Z_scope. |