diff options
| author | Cyril Cohen | 2019-11-24 19:29:51 +0100 |
|---|---|---|
| committer | GitHub | 2019-11-24 19:29:51 +0100 |
| commit | f43a928dc62abd870c3b15b4147b2ad76029b701 (patch) | |
| tree | ff15297daccd6ebf00310eb11af0d82e74453eda /mathcomp | |
| parent | bc5ee7beb4011bf0ea4734cfc99fda24ee2eb9e6 (diff) | |
| parent | bd308dab655e37275afc3fd33ed80cb73647a9ae (diff) | |
Merge pull request #438 from pi8027/hint-database
Fix hint declarations to specify the database explicitly
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 5c2ad4c..6f7c5b5 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -2257,7 +2257,7 @@ suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|. elim: k => [|k IHk] k_lt //=; apply: (leq_ltn_trans (IHk (ltnW k_lt))). by rewrite proper_card// properEneq// subset_iterS neq_iter. Qed. -Hint Resolve fixsetK. +Hint Resolve fixsetK : core. Lemma minset_fix : minset [pred X | F X == X] fixset. Proof. @@ -2338,7 +2338,7 @@ Hypothesis (F_mono : {homo F : X Y / X \subset Y}). Definition funsetC X := ~: (F (~: X)). Lemma funsetC_mono : {homo funsetC : X Y / X \subset Y}. Proof. by move=> *; rewrite subCset setCK F_mono// subCset setCK. Qed. -Hint Resolve funsetC_mono. +Hint Resolve funsetC_mono : core. Definition cofixset := ~: fixset funsetC. |