diff options
Diffstat (limited to 'test-suite/parser/obj_magic.v')
| -rw-r--r-- | test-suite/parser/obj_magic.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v index 6cdbdd13f6..aeb975b59a 100644 --- a/test-suite/parser/obj_magic.v +++ b/test-suite/parser/obj_magic.v @@ -15,6 +15,7 @@ Prolog [A (B c)] 4. EApply H with 1:= H2 a:= b. Inversion H using (A b). Inversion H using (A b) in H1 H2. +Ring a b. Hint Rewrite -> [ (A b) ] in v. Hint Rewrite <- [ (A b) ] in v using Auto. |