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/FMapList.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/FMapList.v')
| -rw-r--r-- | theories/FSets/FMapList.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index a5c00189c4..204e8d0199 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -51,6 +51,7 @@ Proof. intro abs. inversion abs. Qed. +#[local] Hint Resolve empty_1 : core. Lemma empty_sorted : Sort empty. @@ -216,6 +217,7 @@ Proof. compute in H0,H1. simpl; case (X.compare x x''); intuition. Qed. +#[local] Hint Resolve add_Inf : core. Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m). @@ -302,6 +304,7 @@ Proof. inversion_clear Hm. apply Inf_lt with (x'',e''); auto. Qed. +#[local] Hint Resolve remove_Inf : core. Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m). @@ -586,6 +589,7 @@ Proof. inversion_clear H; auto. Qed. +#[local] Hint Resolve map_lelistA : core. Lemma map_sorted : forall (m: t elt)(Hm : sort (@ltk elt) m)(f:elt -> elt'), @@ -655,6 +659,7 @@ Proof. inversion_clear H; auto. Qed. +#[local] Hint Resolve mapi_lelistA : core. Lemma mapi_sorted : forall m (Hm : sort (@ltk elt) m)(f: key ->elt -> elt'), @@ -782,6 +787,7 @@ Proof. inversion_clear H; auto. inversion_clear H0; auto. Qed. +#[local] Hint Resolve combine_lelistA : core. Lemma combine_sorted : |