diff options
Diffstat (limited to 'test-suite/parser')
| -rw-r--r-- | test-suite/parser/obj_magic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v index 6de2f8c7f3..c919d6d8d5 100644 --- a/test-suite/parser/obj_magic.v +++ b/test-suite/parser/obj_magic.v @@ -6,8 +6,8 @@ injection H. replace a with b. rewrite <- H with (a := b). rewrite <- H with (a := b) in H1. -conditional auto rewrite H with (1 := b). -conditional auto rewrite H with (1 := b) in H2. +conditional (auto) rewrite H with (1 := b). +conditional (auto) rewrite H with (1 := b) in H2. dependent rewrite H. cutrewrite (a = b). cutrewrite (a = b) in H. |