diff options
| author | Cyril Cohen | 2020-11-12 15:33:16 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-12 15:33:16 +0100 |
| commit | 8bc77452290bba1f0c8f4eab47676fcffc29b876 (patch) | |
| tree | c933f4a20118c7f38b39a20fd7960395311ca6d0 | |
| parent | d0449f7e13f06ab7295f6919d1701e8adfa72d61 (diff) | |
| parent | de89e39ec1104d7b893d3aa4610fe50cbefabc51 (diff) | |
Merge pull request #641 from pi8027/hint-extern-exact
Replace `exact:` with `apply:` in `Hint Extern` declarations
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index a2a2395..185d5c1 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1584,7 +1584,7 @@ Arguments ltr01 {R}. Arguments normr_idP {R x}. Arguments normr0P {R V v}. Hint Resolve ler01 ltr01 ltr0Sn ler0n : core. -Hint Extern 0 (is_true (0 <= norm _)) => exact: normr_ge0 : core. +Hint Extern 0 (is_true (0 <= norm _)) => apply: normr_ge0 : core. Section NumDomainOperationTheory. @@ -2977,7 +2977,7 @@ Definition lter_nnormr := (ler_nnorml, ltr_nnorml). End NormedZmoduleTheory. -Hint Extern 0 (is_true (norm _ \is real)) => exact: normr_real : core. +Hint Extern 0 (is_true (norm _ \is real)) => apply: normr_real : core. Lemma real_ler_norml x y : x \is real -> (`|x| <= y) = (- y <= x <= y). Proof. |