From 3c75bd3f0e1106be0d238897c4df34ceb5dd811b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 7 Apr 2017 12:00:04 -0400 Subject: Make dlet-moving on sigma goals use change Replace with abstract blocks reduction of the first projection. --- src/Util/Tactics/MoveLetIn.v | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'src/Util/Tactics') 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 := -- cgit v1.2.3