diff options
| -rw-r--r-- | test-suite/bugs/closed/3944.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3944.v b/test-suite/bugs/closed/3944.v index 4cc511ac71..58e60f4f2e 100644 --- a/test-suite/bugs/closed/3944.v +++ b/test-suite/bugs/closed/3944.v @@ -2,4 +2,4 @@ Require Import Setoid. Definition C (T : Type) := T. Goal forall T (i : C T) (v : T), True. Proof. -setoid_rewrite plus_n_Sm. +Fail setoid_rewrite plus_n_Sm. |