Skip to content

Commit

Permalink
Fix the remaining fragile-hint-constr warning
Browse files Browse the repository at this point in the history
  • Loading branch information
Columbus240 committed Aug 21, 2021
1 parent da101d6 commit fdda7fe
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion theories/ZornsLemma/InverseImage.v
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ apply Extensionality_Ensembles; split; red; intros.
constructor; trivial.
Qed.

Global Hint Resolve @inverse_image_increasing : sets.
Global Hint Resolve inverse_image_increasing : sets.
Hint Rewrite @inverse_image_empty @inverse_image_full
@inverse_image_intersection @inverse_image_union
@inverse_image_complement @inverse_image_composition : sets.
Expand Down

0 comments on commit fdda7fe

Please sign in to comment.