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/btauto | |
| 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/btauto')
| -rw-r--r-- | theories/btauto/Algebra.v | 6 | ||||
| -rw-r--r-- | theories/btauto/Reflect.v | 2 |
2 files changed, 8 insertions, 0 deletions
diff --git a/theories/btauto/Algebra.v b/theories/btauto/Algebra.v index 4a603f2c52..08bb49a449 100644 --- a/theories/btauto/Algebra.v +++ b/theories/btauto/Algebra.v @@ -10,6 +10,7 @@ end. Arguments decide P /H. +#[global] Hint Extern 5 => progress bool : core. Ltac define t x H := @@ -147,6 +148,7 @@ Qed. (** * The core reflexive part. *) +#[local] Hint Constructors valid : core. Fixpoint beq_poly pl pr := @@ -315,6 +317,7 @@ Section Validity. (* Decision procedure of validity *) +#[local] Hint Constructors valid linear : core. Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p. @@ -414,6 +417,7 @@ intros pl; induction pl; intros pr var; simpl. rewrite poly_add_compat, poly_mul_mon_compat, IHpl1, IHpl2; ring. Qed. +#[local] Hint Extern 5 => match goal with | [ |- (Pos.max ?x ?y <= ?z)%positive ] => @@ -426,8 +430,10 @@ match goal with apply Pos.max_case_strong; intros; lia | _ => lia end : core. +#[local] Hint Resolve Pos.le_max_r Pos.le_max_l : core. +#[local] Hint Constructors valid linear : core. (* Compatibility of validity w.r.t algebraic operations *) diff --git a/theories/btauto/Reflect.v b/theories/btauto/Reflect.v index 867fe69550..a653b94d1c 100644 --- a/theories/btauto/Reflect.v +++ b/theories/btauto/Reflect.v @@ -77,9 +77,11 @@ intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto. end. Qed. +#[local] Hint Extern 5 => change 0 with (min 0 0) : core. Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core. Local Hint Constructors valid : core. +#[local] Hint Extern 5 => lia : core. (* Compatibility with validity *) |