diff options
| -rw-r--r-- | src/Reflection/ExprInversion.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v index c403ed5e6..6a44a87aa 100644 --- a/src/Reflection/ExprInversion.v +++ b/src/Reflection/ExprInversion.v @@ -137,3 +137,15 @@ Global Arguments invert_LetIn {_ _ _ _} _. Global Arguments invert_Pair {_ _ _ _ _} _. Global Arguments invert_Abs {_ _ _ _ _} _ _. Global Arguments invert_Return {_ _ _ _} _. + +Ltac invert_expr_subst_step := + match goal with + | _ => progress subst + | [ H : invert_Var ?e = Some _ |- _ ] => apply invert_Var_Some in H + | [ H : invert_Op ?e = Some _ |- _ ] => apply invert_Op_Some in H + | [ H : invert_LetIn ?e = Some _ |- _ ] => apply invert_LetIn in H + | [ H : invert_Pair ?e = Some _ |- _ ] => apply invert_Pair_Some in H + | [ H : invert_Abs ?e = _ |- _ ] => apply invert_Abs_Some in H + | [ H : invert_Return ?e = _ |- _ ] => apply invert_Return_Some in H + end. +Ltac invert_expr_subst := repeat invert_expr_subst_step. |