diff options
Diffstat (limited to 'test-suite/parser')
| -rw-r--r-- | test-suite/parser/obj_magic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v index c919d6d8d5..7d60bbd977 100644 --- a/test-suite/parser/obj_magic.v +++ b/test-suite/parser/obj_magic.v @@ -1,5 +1,5 @@ inversion H. -ry absurd (exists a : b, c). +try absurd (exists a : b, c). discriminate H. simplify_eq H. injection H. |