pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Make [sets] tactic more robust to type synonyms

Browse source
This commit is contained in:
Adam Chlipala 2017-05-14 12:50:18 -04:00
parent 962936a80d
commit 9550a02a37
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
FrapWithoutSets.v
View file

@ -234,6 +234,10 @@ Qed.
Ltac sets0 := Sets.sets ltac:(simpl in *; intuition (subst; auto; try equality; try linear_arithmetic)).
Ltac sets := propositional;
try match goal with
| [ |- @eq (?T -> Prop) _ _ ] =>
change (T -> Prop) with (set T)
end;
try match goal with
| [ |- @eq (set _) _ _ ] =>
let x := fresh "x" in