From e5fb9c5cbce5e7e7e8fcb3d82c45074f9c165158 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 11:56:19 +0100
Subject: 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.
---
 doc/sphinx/addendum/micromega.rst | 5 +++--
 1 file 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.
-- 
cgit v1.2.3