diff options
| author | Kazuhiko Sakaguchi | 2020-11-12 17:51:18 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-11-12 17:54:51 +0900 |
| commit | de89e39ec1104d7b893d3aa4610fe50cbefabc51 (patch) | |
| tree | c933f4a20118c7f38b39a20fd7960395311ca6d0 /mathcomp/algebra | |
| parent | d0449f7e13f06ab7295f6919d1701e8adfa72d61 (diff) | |
It is prohibited to use `exact:` in a `Hint Extern`
since `exact` might call `ssrdone` which calls use of level 0 hints, potentially
causing a loop in some weird cases.
Diffstat (limited to 'mathcomp/algebra')
| -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. |