Add invert_match_expr

1 files changed, 14 insertions, 0 deletions

diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index 3d0caa0cb..fa3dd945e 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -156,6 +156,20 @@ Ltac invert_expr_step :=
 
 Ltac invert_expr := repeat invert_expr_step.
 
+Ltac invert_match_expr_step :=
+  match goal with
+  | [ |- appcontext[match ?e with TT => _ | _ => _ end] ]
+    => invert_one_expr e
+  | [ |- appcontext[match ?e with Abs _ _ _ => _ | _ => _ end] ]
+    => invert_one_expr e
+  | [ H : appcontext[match ?e with TT => _ | _ => _ end] |- _ ]
+    => invert_one_expr e
+  | [ H : appcontext[match ?e with Abs _ _ _ => _ | _ => _ end] |- _ ]
+    => invert_one_expr e
+  end.
+
+Ltac invert_match_expr := repeat invert_match_expr_step.
+
 Ltac invert_expr_subst_step :=
   match goal with
   | [ H : invert_Var ?e = Some _ |- _ ] => apply invert_Var_Some in H