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/micromega | |
| 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/micromega')
| -rw-r--r-- | theories/micromega/Tauto.v | 3 | ||||
| -rw-r--r-- | theories/micromega/ZArith_hints.v | 22 |
2 files changed, 25 insertions, 0 deletions
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index 99af214396..ce12b02359 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -1562,6 +1562,7 @@ Section S. auto. Qed. + #[local] Hint Resolve no_middle_eval_tt : tauto. Lemma or_clause_correct : forall cl cl' env, eval_opt_clause env (or_clause cl cl') <-> eval_clause env cl \/ eval_clause env cl'. @@ -1702,6 +1703,7 @@ Section S. intros k; destruct k ; simpl; auto. Qed. + #[local] Hint Resolve hold_eTT : tauto. Lemma hold_eFF : forall k, @@ -1710,6 +1712,7 @@ Section S. intros k; destruct k ; simpl;auto. Qed. + #[local] Hint Resolve hold_eFF : tauto. Lemma hold_eAND : forall k r1 r2, diff --git a/theories/micromega/ZArith_hints.v b/theories/micromega/ZArith_hints.v index a6d3d92a99..3545e8b218 100644 --- a/theories/micromega/ZArith_hints.v +++ b/theories/micromega/ZArith_hints.v @@ -10,34 +10,56 @@ Require Import Lia. Import ZArith_base. +#[global] Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r Z.mul_add_distr_l: zarith. Require Export Zhints. +#[global] Hint Extern 10 (_ = _ :>nat) => abstract lia: zarith. +#[global] Hint Extern 10 (_ <= _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ < _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ >= _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ > _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ <> _ :>nat) => abstract lia: zarith. +#[global] Hint Extern 10 (~ _ <= _) => abstract lia: zarith. +#[global] Hint Extern 10 (~ _ < _) => abstract lia: zarith. +#[global] Hint Extern 10 (~ _ >= _) => abstract lia: zarith. +#[global] Hint Extern 10 (~ _ > _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ = _ :>Z) => abstract lia: zarith. +#[global] Hint Extern 10 (_ <= _)%Z => abstract lia: zarith. +#[global] Hint Extern 10 (_ < _)%Z => abstract lia: zarith. +#[global] Hint Extern 10 (_ >= _)%Z => abstract lia: zarith. +#[global] Hint Extern 10 (_ > _)%Z => abstract lia: zarith. +#[global] Hint Extern 10 (_ <> _ :>Z) => abstract lia: zarith. +#[global] Hint Extern 10 (~ (_ <= _)%Z) => abstract lia: zarith. +#[global] Hint Extern 10 (~ (_ < _)%Z) => abstract lia: zarith. +#[global] Hint Extern 10 (~ (_ >= _)%Z) => abstract lia: zarith. +#[global] Hint Extern 10 (~ (_ > _)%Z) => abstract lia: zarith. +#[global] Hint Extern 10 False => abstract lia: zarith. |