diff options
| author | Pierre-Marie Pédrot | 2015-02-16 09:44:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-16 09:44:51 +0100 |
| commit | ec50702d19587d450ffc36afc03a4d48ba0880e3 (patch) | |
| tree | 556d960dc4874a893732f1dd5101b58757642f95 | |
| parent | 8f0897cd520b28501fc5455524ab588998bcbb30 (diff) | |
Fixing test for bug #3944.
| -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. |