Commit bb3e9abf authored by Michael Sammler's avatar Michael Sammler
Browse files

different liUnfoldLetGoal

parent b6a5bb68
Pipeline #57792 failed with stage
in 6 minutes and 24 seconds
......@@ -308,13 +308,11 @@ Tactic Notation "li_let_bind" constr(T) tactic3(tac) :=
Ltac liUnfoldLetGoal :=
match goal with
| |- envs_entails _ ?P =>
let rec go P tac :=
match P with
| ?Q ?R => go Q tac
| _ => is_var P; tac P
end in
go P ltac:(fun P => unfold LET_ID in P; unfold P; try clear P)
let h := get_head P in
is_var P;
unfold LET_ID in P;
unfold P;
try clear P
(* lazymatch goal with *)
(* | |- envs_entails ?Δ ?P => *)
(* let h := get_head P in *)
......
Markdown is supported
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