diff options
Diffstat (limited to 'test-suite/parser/obj_magic.v')
| -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 7d60bbd977..7f0c23af66 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. +rewrite H with (1 := b). +rewrite H with (1 := b) in H2. dependent rewrite H. cutrewrite (a = b). cutrewrite (a = b) in H. |