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

unfold lets before solving evars

parent 582c126c
Pipeline #57804 passed with stage
in 11 minutes and 22 seconds
......@@ -423,7 +423,7 @@ Ltac solve_protected_eq :=
(* intros because it is less aggressive than move => * *)
intros;
solve_protected_eq_unfold_tac;
repeat rewrite protected_eq;
liUnfoldLetsInContext;
liUnfoldAllEvars;
lazymatch goal with |- ?a = ?b => unify a b with solve_protected_eq_db end;
exact: eq_refl.
......
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