Comment out examples requiring CSDP

math-comp · May 11, 2022 · ed2ba79 · ed2ba79
1 parent b085883
commit ed2ba79
Showing 1 changed file with 8 additions and 4 deletions.
diff --git a/examples/lra_examples.v b/examples/lra_examples.v
@@ -219,8 +219,10 @@ Qed.
 Goal forall x, -x^+2 >= 0 -> x - 1 >= 0 -> False.
 Proof.
 move=> *.
-psatz 3.
-Qed.
+(* Requires CSDP *)
+(* psatz 3. *)
+(* Qed. *)
+Abort.
 
 Goal forall x, -x^+2 >= 0 -> x - 1 >= 0 -> False.
 Proof.
@@ -232,8 +234,10 @@ Lemma motzkin' x y :
   (x^+2 + y^+2 + 1) * (x^+2 * y^+4 + x^+4*y^+2 + 1 - 3%:R * x^+2 * y^+2) >= 0.
 Proof.
 move=> *.
-psatz 3.
-Qed.
+(* Requires CSDP *)
+(* psatz 3. *)
+(* Qed. *)
+Abort.
 
 Goal forall x, -x^+2 >= 0 -> x - 1 >= 0 -> False.
 Proof.