diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-07 12:00:04 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-07 12:00:04 -0400 |
| commit | 3c75bd3f0e1106be0d238897c4df34ceb5dd811b (patch) | |
| tree | 56878ec6d92c83173b8b41b375efa0dc740d19b4 /src/Util/Tactics | |
| parent | e7a7d97ff871d672b60a8f7e1ed73b9e263e121c (diff) | |
Make dlet-moving on sigma goals use change
Replace with abstract blocks reduction of the first projection.
Diffstat (limited to 'src/Util/Tactics')
| -rw-r--r-- | src/Util/Tactics/MoveLetIn.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/Util/Tactics/MoveLetIn.v b/src/Util/Tactics/MoveLetIn.v index a0ef910b2..c5ec3d8a8 100644 --- a/src/Util/Tactics/MoveLetIn.v +++ b/src/Util/Tactics/MoveLetIn.v @@ -7,8 +7,7 @@ Ltac sig_dlet_in_rhs_to_context_step v := lazymatch goal with | [ |- { a | _ = @Let_In ?A ?B ?x _ } ] => pose x as v; - replace (@Let_In A B x) with (fun P : forall a : A, B a => P v) - by (clear; abstract (subst v; cbv [Let_In]; reflexivity)); + change (@Let_In A B x) with (fun P : forall a : A, B a => P v); cbv beta end. Ltac sig_dlet_in_rhs_to_context := @@ -20,8 +19,7 @@ Ltac sig_dlet_in_lhs_to_context_step v := lazymatch goal with | [ |- { a | @Let_In ?A ?B ?x _ = _ } ] => pose x as v; - replace (@Let_In A B x) with (fun P : forall a : A, B a => P v) - by (clear; abstract (subst v; cbv [Let_In]; reflexivity)); + change (@Let_In A B x) with (fun P : forall a : A, B a => P v); cbv beta end. Ltac sig_dlet_in_lhs_to_context := @@ -32,8 +30,7 @@ Ltac goal_dlet_to_context_step v := match goal with | [ |- context[@Let_In ?A ?B ?x] ] => pose x as v; - replace (@Let_In A B x) with (fun P : forall a : A, B a => P v) - by (clear; abstract (subst v; cbv [Let_In]; reflexivity)); + change (@Let_In A B x) with (fun P : forall a : A, B a => P v); cbv beta end. Ltac goal_dlet_to_context := |