diff options
| author | Pierre-Marie Pédrot | 2020-11-14 17:55:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-16 12:28:27 +0100 |
| commit | 68cd077344ce37db1a601079dbc4fdcae6c8d41f (patch) | |
| tree | edcad8a440c4fb61256ff26d5554dd17b8d03423 /theories/FSets/FSetBridge.v | |
| parent | 7daf04e53bdee6b0c9d0171c1e0d05903d677d3a (diff) | |
Explicitly annotate all hint declarations of the standard library.
By default Coq stdlib warnings raise an error, so this is really required.
Diffstat (limited to 'theories/FSets/FSetBridge.v')
| -rw-r--r-- | theories/FSets/FSetBridge.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 73021a84a3..4917fcb5fd 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -137,6 +137,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder. Qed. + #[global] Hint Resolve compat_P_aux : core. Definition filter : @@ -467,6 +468,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Proof. intros; unfold elements; case (M.elements s); firstorder. Qed. + #[global] Hint Resolve elements_3 : core. Lemma elements_3w : forall s : t, NoDupA E.eq (elements s). @@ -666,6 +668,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. rewrite <- H1; firstorder. Qed. + #[global] Hint Resolve compat_P_aux : core. Definition filter (f : elt -> bool) (s : t) : t := |