diff options
Diffstat (limited to 'test-suite/failure/ClearBody.v')
| -rw-r--r-- | test-suite/failure/ClearBody.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/failure/ClearBody.v b/test-suite/failure/ClearBody.v index 609d5b3b..e321e59f 100644 --- a/test-suite/failure/ClearBody.v +++ b/test-suite/failure/ClearBody.v @@ -5,4 +5,4 @@ Goal True. set (n := 0) in *. set (I := refl_equal 0) in *. change (n = 0) in (type of I). -clearbody n. +Fail clearbody n. |