Commit 7fd3e339 authored by Michael Sammler's avatar Michael Sammler
Browse files

unfold lets before instantiating evars

parent 74787074
Pipeline #57807 passed with stage
in 11 minutes and 39 seconds
......@@ -350,6 +350,7 @@ Ltac create_protected_evar A :=
Ltac unfold_instantiated_evar_hook H := idtac.
Ltac unfold_instantiated_evar H :=
liUnfoldLetsInContext;
unfold_instantiated_evar_hook H;
revert H;
repeat match goal with
......
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