diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-23 17:36:44 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-23 17:36:44 -0500 |
commit | 3f4200782e33e6ee3523b7e5a5787008a1e036ca (patch) | |
tree | 7b9ccb1cece4c29ec5e717dea5dd494fce960e95 /src/Reflection | |
parent | 19797bd0eb8cc1b879562728da63255dafcde893 (diff) |
Better invert_expr
Diffstat (limited to 'src/Reflection')
-rw-r--r-- | src/Reflection/ExprInversion.v | 5 |
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 |