Commit 51b58582 authored by Michael Sammler's avatar Michael Sammler
Browse files

liUnfoldLetGoal also beneath bi_sep

parent f6062611
Pipeline #57811 passed with stage
in 11 minutes and 27 seconds
...@@ -308,16 +308,19 @@ Tactic Notation "li_let_bind" constr(T) tactic3(tac) := ...@@ -308,16 +308,19 @@ Tactic Notation "li_let_bind" constr(T) tactic3(tac) :=
(* unfold_let_goal_tac lets users unfold custom definitions. *) (* unfold_let_goal_tac lets users unfold custom definitions. *)
Ltac unfold_let_goal_tac H := idtac. Ltac unfold_let_goal_tac H := idtac.
Ltac liUnfoldLetGoal := Ltac liUnfoldLetGoal :=
match goal with let do_unfold P :=
| |- envs_entails _ ?P => let H := get_head P in
let H := get_head P in is_var H;
is_var H; unfold LET_ID in H;
unfold LET_ID in H; unfold_let_goal_tac H;
unfold_let_goal_tac H; (* This unfold inserts a cast but that is not too bad for
(* This unfold inserts a cast but that is not too bad for performance since the goal is small at this point. *)
performance since the goal is small at this point. *) unfold H;
unfold H; try clear H
try clear H in
lazymatch goal with
| |- envs_entails _ (?P _) => do_unfold P
| |- envs_entails _ ?P => do_unfold P
end. end.
Ltac liUnfoldLetsContaining H := Ltac liUnfoldLetsContaining H :=
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment