From 397fb9dfbe09b85d8cbeed5854134a6491372ae4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 29 Jun 2020 17:38:15 +0200
Subject: [test-suite] async-proofs off in tests with Fail Timeout

Apparently the `Timeout` exception is raised by a signal handled, and
that can happen when the running thread is a worker manager, rather than
the main thread (the one that should be interrupted).

Given that the point of these tests is to test *auto and not the STM,
we disable async proofs forcibly.
---
 test-suite/success/Typeclasses.v | 1 +
 test-suite/success/auto.v        | 1 +
 test-suite/success/bteauto.v     | 1 +
 3 files changed, 3 insertions(+)

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 66305dfefa..563651cfa5 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-async-proofs" "off") *)
 Module applydestruct.
   Class Foo (A : Type) :=
     { bar : nat -> A;
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index 62a66daf7d..98e2917300 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-async-proofs" "off") *)
 (* Wish #2154 by E. van der Weegen *)
 
 (* auto was not using f_equal-style lemmas with metavariables occurring
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index cea7d92c0b..9577d63f61 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-async-proofs" "off") *)
 Require Import Program.Tactics.
 Module Backtracking.
   Class A := { foo : nat }.
-- 
cgit v1.2.3