diff options
Diffstat (limited to 'src/Compilers/ExprInversion.v')
| -rw-r--r-- | src/Compilers/ExprInversion.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Compilers/ExprInversion.v b/src/Compilers/ExprInversion.v index a1d2587f5..48ea30907 100644 --- a/src/Compilers/ExprInversion.v +++ b/src/Compilers/ExprInversion.v @@ -174,13 +174,13 @@ Ltac invert_expr := repeat invert_expr_step. Ltac invert_match_expr_step := match goal with - | [ |- appcontext[match ?e with TT => _ | _ => _ end] ] + | [ |- context[match ?e with TT => _ | _ => _ end] ] => invert_one_expr e - | [ |- appcontext[match ?e with Abs _ _ _ => _ end] ] + | [ |- context[match ?e with Abs _ _ _ => _ end] ] => invert_one_expr e - | [ H : appcontext[match ?e with TT => _ | _ => _ end] |- _ ] + | [ H : context[match ?e with TT => _ | _ => _ end] |- _ ] => invert_one_expr e - | [ H : appcontext[match ?e with Abs _ _ _ => _ end] |- _ ] + | [ H : context[match ?e with Abs _ _ _ => _ end] |- _ ] => invert_one_expr e end. |