diff options
| author | Gaëtan Gilbert | 2020-07-01 11:47:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 11:47:31 +0200 |
| commit | 144d121ad9a5b2aead25f9365021a9753a835e12 (patch) | |
| tree | 8194dcb2769e0bbda69c202ead0dbcbe45b671eb | |
| parent | d1407a5adabf600f3a80b2715fcae1ecd7a5df93 (diff) | |
| parent | 397fb9dfbe09b85d8cbeed5854134a6491372ae4 (diff) | |
Merge PR #12605: [test-suite] async-proofs off in tests with Fail Timeout
Reviewed-by: SkySkimmer
| -rw-r--r-- | test-suite/success/Typeclasses.v | 1 | ||||
| -rw-r--r-- | test-suite/success/auto.v | 1 | ||||
| -rw-r--r-- | test-suite/success/bteauto.v | 1 |
3 files changed, 3 insertions, 0 deletions
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 }. |