diff options
author | 2015-02-16 09:44:51 +0100 | |
---|---|---|
committer | 2015-02-16 09:44:51 +0100 | |
commit | ec50702d19587d450ffc36afc03a4d48ba0880e3 (patch) | |
tree | 556d960dc4874a893732f1dd5101b58757642f95 /test-suite/bugs/closed/3944.v | |
parent | 8f0897cd520b28501fc5455524ab588998bcbb30 (diff) |
Fixing test for bug #3944.
Diffstat (limited to 'test-suite/bugs/closed/3944.v')
-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 4cc511ac7..58e60f4f2 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. |