Better invert_expr

1 files changed, 5 insertions, 0 deletions

diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index 6bf813bf7..9fc373a74 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -144,6 +144,11 @@ Ltac invert_expr_subst_step :=
   | [ H : invert_Op ?e = Some _ |- _ ] => apply invert_Op_Some in H
   | [ H : invert_LetIn ?e = Some _ |- _ ] => apply invert_LetIn_Some in H
   | [ H : invert_Pair ?e = Some _ |- _ ] => apply invert_Pair_Some in H
+  | [ e : expr _ _ (Arrow _ _) |- _ ]
+    => let f := fresh e in
+       let H := fresh in
+       remember (invert_Abs e) as f eqn:H;
+       apply invert_Abs_Some in H
   | [ H : invert_Abs ?e = _ |- _ ] => apply invert_Abs_Some in H
   | [ H : invert_Return ?e = _ |- _ ] => apply invert_Return_Some in H
   | _ => progress subst