Commit 3ffcf4e0 authored by Michael Sammler's avatar Michael Sammler
Browse files

unfold even more lets

parent 7fd3e339
Pipeline #57808 passed with stage
in 11 minutes and 33 seconds
......@@ -350,6 +350,7 @@ Ltac create_protected_evar A :=
Ltac unfold_instantiated_evar_hook H := idtac.
Ltac unfold_instantiated_evar H :=
(* Necessary because the lets might contain evars. *)
liUnfoldLetsInContext;
unfold_instantiated_evar_hook H;
revert H;
......@@ -383,6 +384,8 @@ Ltac unfold_instantiated_evar H :=
It can use _ to create new evars, but they should be surrounded by [protected (EVAR_ID _)] such that instantiate_protected can find them and create the right let bindings afterwards.
*)
Ltac instantiate_protected H' tac_with :=
(* Necessary because the lets might contain evars. *)
liUnfoldLetsInContext;
lazymatch H' with
| protected ?H =>
unfold EVAR_ID in 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