diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-23 16:05:57 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-23 16:05:57 -0500 |
commit | 4cc2a1f73c68f77c28f75c0d583ed05a443da1d7 (patch) | |
tree | 6f2e398fb48a814290930925ca9e4a8670b52a42 /src | |
parent | eca8e733e15c19ab2e56734f1671f658af690045 (diff) |
Add invert_expr_subst
Diffstat (limited to 'src')
-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. |