diff options
| author | Jason Gross | 2019-11-26 13:27:56 -0500 |
|---|---|---|
| committer | GitHub | 2019-11-26 13:27:56 -0500 |
| commit | 73bb54d1625ae6eafdb9eb7f2c673fb039150fdb (patch) | |
| tree | e84fd963628e6c1f6f3500eeefbda4c56ed17f16 /test-suite/complexity/pattern.v | |
| parent | f269ffd88b6a725d8f8f6a7bf1e91799b361a31f (diff) | |
Update test-suite/complexity/pattern.v
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
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 := (_ = _). |