diff options
| author | Jasper Hugunin | 2018-02-21 23:27:04 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2018-02-21 23:27:04 -0800 |
| commit | 64ceb784611e5ded0c715835a36490de1c3bb1ca (patch) | |
| tree | 105ff4785b1ac83c081d04379423451fb84ac257 /mathcomp/algebra/interval.v | |
| parent | 181e9e94e04f45e0deb231246e1783c48be4f99d (diff) | |
Change Implicit Arguments to Arguments in algebra
Diffstat (limited to 'mathcomp/algebra/interval.v')
| -rw-r--r-- | mathcomp/algebra/interval.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index e269752..b699da1 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -134,7 +134,7 @@ Lemma itv_dec : forall (x : R) (i : interval R), reflect (itv_decompose i x) (x \in i). Proof. by move=> x [[[] a|] [[] b|]]; apply: (iffP andP); case. Qed. -Implicit Arguments itv_dec [x i]. +Arguments itv_dec [x i]. Definition lersif (x y : R) b := if b then x < y else x <= y. @@ -243,7 +243,7 @@ move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //; Qed. Hint Rewrite intP. -Implicit Arguments itvP [x i]. +Arguments itvP [x i]. Definition subitv (i1 i2 : interval R) := match i1, i2 with |