diff options
| -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 }. |