From 73bb54d1625ae6eafdb9eb7f2c673fb039150fdb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 26 Nov 2019 13:27:56 -0500 Subject: Update test-suite/complexity/pattern.v Co-Authored-By: Hugo Herbelin --- test-suite/complexity/pattern.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 := (_ = _). -- cgit v1.2.3