From 9550a02a37c15111585c191b604bfb49899f0c54 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 14 May 2017 12:50:18 -0400 Subject: [PATCH] Make [sets] tactic more robust to type synonyms --- FrapWithoutSets.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v index ae8e051..01e29b3 100644 --- a/FrapWithoutSets.v +++ b/FrapWithoutSets.v @@ -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