diff options
| author | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
| commit | 22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (patch) | |
| tree | f4b84d2114aa4523aebf62f020ae46f4321fb10a /theories/FSets/FSetInterface.v | |
| parent | ba8e3caa31e464d1007c4ad54e8d70fd70ca3300 (diff) | |
| parent | eeb1d861551e25c6a92721334b3c9f36b7ebb012 (diff) | |
Merge PR #8987: Deprecate hint declaration/removal with no specified database
Diffstat (limited to 'theories/FSets/FSetInterface.v')
| -rw-r--r-- | theories/FSets/FSetInterface.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index 0926d3ae9f..fa7f1c5f4e 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -253,7 +253,7 @@ Module Type WSfun (E : DecidableType). End Spec. - Hint Transparent elt. + Hint Transparent elt : core. Hint Resolve mem_1 equal_1 subset_1 empty_1 is_empty_1 choose_1 choose_2 add_1 add_2 remove_1 remove_2 singleton_2 union_1 union_2 union_3 |