Skip to content
Snippets Groups Projects
Commit b9af598b authored by Ralf Jung's avatar Ralf Jung
Browse files

port tweak from gen_proofmode branch

parent e87e7178
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
theories/lang/lifting.v
+ 2
− 2
View file @ b9af598b
......@@ -19,8 +19,8 @@ Global Opaque iris_invG.
Ltac inv_lit :=
repeat match goal with
| H : lit_eq _ ?x ?y |- _ => inversion H; clear H; simplify_eq/=
| H : lit_neq ?x ?y |- _ => inversion H; clear H; simplify_eq/=
| H : lit_eq _ ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
| H : lit_neq ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
end.
Ltac inv_bin_op_eval :=
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment