Minor additions

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index 0cb35f4b7..6bf813bf7 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -140,12 +140,12 @@ 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_Some 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
+  | _ => progress subst
   end.
 Ltac invert_expr_subst := repeat invert_expr_subst_step.