diff options
Diffstat (limited to 'test-suite/complexity/pattern.v')
| -rw-r--r-- | test-suite/complexity/pattern.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/complexity/pattern.v b/test-suite/complexity/pattern.v index 14e388cd75..fb5bf5a00b 100644 --- a/test-suite/complexity/pattern.v +++ b/test-suite/complexity/pattern.v @@ -24,7 +24,7 @@ Ltac do_time_to n := | ?n' => do_time_to (Nat.div2 n'); idtac n'; do_time n' end. -Local Set Warnings Append "-abstract-large-number". +Local Set Warnings "-abstract-large-number". (* Don't spend lots of time printing *) Notation hide := (_ = _). |