diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/choice.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/div.v | 3 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 32 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finfun.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 80 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 39 | ||||
| -rw-r--r-- | mathcomp/ssreflect/generic_quotient.v | 17 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 11 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 34 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 4 |
13 files changed, 115 insertions, 133 deletions
diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index 9e7c77f..baa7231 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -562,8 +562,8 @@ Export Countable.Exports. Definition unpickle T := Countable.unpickle (Countable.class T). Definition pickle T := Countable.pickle (Countable.class T). -Arguments unpickle [T]. -Prenex Implicits pickle unpickle. +Arguments unpickle {T}. +Prenex Implicits pickle. Section CountableTheory. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 6565ddf..ed1eedf 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -302,8 +302,7 @@ Proof. apply: (iffP eqP) => [md0 | [k ->]]; last by rewrite modnMl. by exists (m %/ d); rewrite {1}(divn_eq m d) md0 addn0. Qed. -Arguments dvdnP [d m]. -Prenex Implicits dvdnP. +Arguments dvdnP {d m}. Lemma dvdn0 d : d %| 0. Proof. by case: d. Qed. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 76b0521..4487ab4 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -171,7 +171,7 @@ Proof. by []. Qed. Lemma eqP T : Equality.axiom (@eq_op T). Proof. by case: T => ? []. Qed. -Arguments eqP [T x y]. +Arguments eqP {T x y}. Delimit Scope eq_scope with EQ. Open Scope eq_scope. @@ -254,8 +254,8 @@ Proof. by rewrite eq_sym; apply: ifN. Qed. End Contrapositives. -Arguments memPn [T1 A x]. -Arguments memPnC [T1 A x]. +Arguments memPn {T1 A x}. +Arguments memPnC {T1 A x}. Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2. Proof. @@ -363,10 +363,10 @@ Proof. by case: eqP; [left | right]. Qed. End EqPred. -Arguments predU1P [T x y b]. -Arguments pred2P [T T2 x y z u]. -Arguments predD1P [T x y b]. -Prenex Implicits pred1 pred2 pred3 pred4 predU1 predC1 predD1 predU1P. +Arguments predU1P {T x y b}. +Arguments pred2P {T T2 x y z u}. +Arguments predD1P {T x y b}. +Prenex Implicits pred1 pred2 pred3 pred4 predU1 predC1 predD1. Notation "[ 'predU1' x & A ]" := (predU1 x [mem A]) (at level 0, format "[ 'predU1' x & A ]") : fun_scope. @@ -597,14 +597,14 @@ Qed. End SubType. Arguments SubType [T P]. -Arguments Sub [T P s]. -Arguments vrefl [T P]. -Arguments vrefl_rect [T P]. +Arguments Sub {T P s}. +Arguments vrefl {T P}. +Arguments vrefl_rect {T P}. Arguments clone_subType [T P] U v [sT] _ [c Urec cK]. -Arguments insub [T P sT]. +Arguments insub {T P sT}. Arguments insubT [T] P [sT x]. -Arguments val_inj [T P sT]. -Prenex Implicits val Sub vrefl vrefl_rect insub insubd val_inj. +Arguments val_inj {T P sT}. +Prenex Implicits val insubd. Local Notation inlined_sub_rect := (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px). @@ -646,8 +646,7 @@ Notation "[ 'newType' 'for' v 'by' rec ]" := (NewType v _ rec vrefl) (at level 0, format "[ 'newType' 'for' v 'by' rec ]") : form_scope. Definition innew T nT x := @Sub T predT nT x (erefl true). -Arguments innew [T nT]. -Prenex Implicits innew. +Arguments innew {T nT}. Lemma innew_val T nT : cancel val (@innew T nT). Proof. by move=> u; apply: val_inj; apply: SubK. Qed. @@ -737,8 +736,7 @@ Proof. by []. Qed. End SubEqType. -Arguments val_eqP [T P sT x y]. -Prenex Implicits val_eqP. +Arguments val_eqP {T P sT x y}. Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T) (at level 0, format "[ 'eqMixin' 'of' T 'by' <: ]") : form_scope. diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 8b85320..9929e82 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -147,8 +147,8 @@ End PlainTheory. Notation family F := (family_mem (fun_of_simpl (fmem F))). Notation ffun_on R := (ffun_on_mem _ (mem R)). -Arguments familyP [aT rT pT F f]. -Arguments ffun_onP [aT rT R f]. +Arguments familyP {aT rT pT F f}. +Arguments ffun_onP {aT rT R f}. (*****************************************************************************) @@ -213,7 +213,7 @@ Qed. End EqTheory. -Arguments supportP [aT rT y D g]. +Arguments supportP {aT rT y D g}. Notation pfamily y D F := (pfamily_mem y (mem D) (fun_of_simpl (fmem F))). Notation pffun_on y D R := (pffun_on_mem y (mem D) (mem R)). diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index baf5efe..c534b7b 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -224,9 +224,9 @@ Notation closure e a := (closure_mem e (mem a)). Prenex Implicits connect root roots. -Arguments dfsP [T g x y]. -Arguments connectP [T e x y]. -Arguments rootP [T e] _ [x y]. +Arguments dfsP {T g x y}. +Arguments connectP {T e x y}. +Arguments rootP [T e] _ {x y}. Notation fconnect f := (connect (coerced_frel f)). Notation froot f := (root (coerced_frel f)). diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 6cff46e..3fd10fa 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -243,8 +243,7 @@ End BasicSetTheory. Definition inE := (in_set, inE). -Arguments set0 [T]. -Prenex Implicits set0. +Arguments set0 {T}. Hint Resolve in_setT. Notation "[ 'set' : T ]" := (setTfor (Phant T)) @@ -827,7 +826,7 @@ Proof. apply: (iffP subsetP) => [sAB | <- x /setIP[] //]. by apply/setP=> x; rewrite inE; apply/andb_idr/sAB. Qed. -Arguments setIidPl [A B]. +Arguments setIidPl {A B}. Lemma setIidPr A B : reflect (A :&: B = B) (B \subset A). Proof. by rewrite setIC; apply: setIidPl. Qed. @@ -955,29 +954,27 @@ Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed. End setOps. -Arguments set1P [T x a]. -Arguments set1_inj [T]. -Arguments set2P [T x a b]. -Arguments setIdP [T x pA pB]. -Arguments setIP [T x A B]. -Arguments setU1P [T x a B]. -Arguments setD1P [T x A b]. -Arguments setUP [T x A B]. -Arguments setDP [T A B x]. -Arguments cards1P [T A]. -Arguments setCP [T x A]. -Arguments setIidPl [T A B]. -Arguments setIidPr [T A B]. -Arguments setUidPl [T A B]. -Arguments setUidPr [T A B]. -Arguments setDidPl [T A B]. -Arguments subsetIP [T A B C]. -Arguments subUsetP [T A B C]. -Arguments subsetDP [T A B C]. -Arguments subsetD1P [T A B x]. -Prenex Implicits set1 set1_inj. -Prenex Implicits set1P set2P setU1P setD1P setIdP setIP setUP setDP. -Prenex Implicits cards1P setCP setIidPl setIidPr setUidPl setUidPr setDidPl. +Arguments set1P {T x a}. +Arguments set1_inj {T}. +Arguments set2P {T x a b}. +Arguments setIdP {T x pA pB}. +Arguments setIP {T x A B}. +Arguments setU1P {T x a B}. +Arguments setD1P {T x A b}. +Arguments setUP {T x A B}. +Arguments setDP {T A B x}. +Arguments cards1P {T A}. +Arguments setCP {T x A}. +Arguments setIidPl {T A B}. +Arguments setIidPr {T A B}. +Arguments setUidPl {T A B}. +Arguments setUidPr {T A B}. +Arguments setDidPl {T A B}. +Arguments subsetIP {T A B C}. +Arguments subUsetP {T A B C}. +Arguments subsetDP {T A B C}. +Arguments subsetD1P {T A B x}. +Prenex Implicits set1. Hint Resolve subsetT_hint. Section setOpsAlgebra. @@ -1018,8 +1015,7 @@ Proof. by rewrite cardsE cardX. Qed. End CartesianProd. -Arguments setXP [fT1 fT2 A1 A2 x1 x2]. -Prenex Implicits setXP. +Arguments setXP {fT1 fT2 A1 A2 x1 x2}. Local Notation imset_def := (fun (aT rT : finType) f mD => [set y in @image_mem aT rT f mD]). @@ -1365,9 +1361,8 @@ Proof. by move=> sAB1 sAB2; rewrite -!imset2_pair imset2S. Qed. End FunImage. -Arguments imsetP [aT rT f D y]. -Arguments imset2P [aT aT2 rT f2 D1 D2 y]. -Prenex Implicits imsetP imset2P. +Arguments imsetP {aT rT f D y}. +Arguments imset2P {aT aT2 rT f2 D1 D2 y}. Section BigOps. @@ -1499,7 +1494,7 @@ Proof. by move=> fK gK; apply: can2_in_imset_pre; apply: in1W. Qed. End CardFunImage. -Arguments imset_injP [aT rT f D]. +Arguments imset_injP {aT rT f D}. Lemma on_card_preimset (aT rT : finType) (f : aT -> rT) (R : pred rT) : {on R, bijective f} -> #|f @^-1: R| = #|R|. @@ -1703,13 +1698,12 @@ End BigSetOps. Arguments bigcup_sup [T I] j [P F]. Arguments bigcup_max [T I] j [U P F]. -Arguments bigcupP [T I x P F]. -Arguments bigcupsP [T I U P F]. +Arguments bigcupP {T I x P F}. +Arguments bigcupsP {T I U P F}. Arguments bigcap_inf [T I] j [P F]. Arguments bigcap_min [T I] j [U P F]. -Arguments bigcapP [T I x P F]. -Arguments bigcapsP [T I U P F]. -Prenex Implicits bigcupP bigcupsP bigcapP bigcapsP. +Arguments bigcapP {T I x P F}. +Arguments bigcapsP {T I U P F}. Section ImsetCurry. @@ -2088,13 +2082,13 @@ End Transversals. End Partitions. -Arguments trivIsetP [T P]. +Arguments trivIsetP {T P}. Arguments big_trivIset_cond [T R idx op] P [K E]. Arguments set_partition_big_cond [T R idx op] P [D K E]. Arguments big_trivIset [T R idx op] P [E]. Arguments set_partition_big [T R idx op] P [D E]. -Prenex Implicits cover trivIset partition pblock trivIsetP. +Prenex Implicits cover trivIset partition pblock. Lemma partition_partition (T : finType) (D : {set T}) P Q : partition P D -> partition Q P -> @@ -2141,7 +2135,7 @@ apply: (iffP forallP) => [minA | [PA minA] B]. by move=> B PB sBA; have:= minA B; rewrite PB sBA /= eqb_id => /eqP. by apply/implyP=> sBA; apply/eqP; apply/eqP/idP=> [-> // | /minA]; apply. Qed. -Arguments minsetP [P A]. +Arguments minsetP {P A}. Lemma minsetp P A : minset P A -> P A. Proof. by case/minsetP. Qed. @@ -2212,7 +2206,7 @@ Qed. End MaxSetMinSet. -Arguments minsetP [T P A]. -Arguments maxsetP [T P A]. -Prenex Implicits minset maxset minsetP maxsetP. +Arguments minsetP {T P A}. +Arguments maxsetP {T P A}. +Prenex Implicits minset maxset. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 8848999..4b2952f 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -820,14 +820,13 @@ End OpsTheory. Hint Resolve subxx_hint. -Arguments pred0P [T P]. -Arguments pred0Pn [T P]. -Arguments subsetP [T A B]. -Arguments subsetPn [T A B]. -Arguments subset_eqP [T A B]. -Arguments card_uniqP [T s]. -Arguments properP [T A B]. -Prenex Implicits pred0P pred0Pn subsetP subsetPn subset_eqP card_uniqP. +Arguments pred0P {T P}. +Arguments pred0Pn {T P}. +Arguments subsetP {T A B}. +Arguments subsetPn {T A B}. +Arguments subset_eqP {T A B}. +Arguments card_uniqP {T s}. +Arguments properP {T A B}. (**********************************************************************) (* *) @@ -927,14 +926,14 @@ Proof. by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if. Qed. End Quantifiers. -Arguments forallP [T P]. -Arguments eqfunP [T rT f1 f2]. -Arguments forall_inP [T D P]. -Arguments eqfun_inP [T rT D f1 f2]. -Arguments existsP [T P]. -Arguments exists_eqP [T rT f1 f2]. -Arguments exists_inP [T D P]. -Arguments exists_eq_inP [T rT D f1 f2]. +Arguments forallP {T P}. +Arguments eqfunP {T rT f1 f2}. +Arguments forall_inP {T D P}. +Arguments eqfun_inP {T rT D f1 f2}. +Arguments existsP {T P}. +Arguments exists_eqP {T rT f1 f2}. +Arguments exists_inP {T D P}. +Arguments exists_eq_inP {T rT D f1 f2}. Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view)) (at level 4, right associativity, format "''exists_in_' view"). @@ -1197,15 +1196,15 @@ Qed. End Image. Prenex Implicits codom iinv. -Arguments imageP [T T' f A y]. -Arguments codomP [T T' f y]. +Arguments imageP {T T' f A y}. +Arguments codomP {T T' f y}. Lemma flatten_imageP (aT : finType) (rT : eqType) A (P : pred aT) (y : rT) : reflect (exists2 x, x \in P & y \in A x) (y \in flatten [seq A x | x in P]). Proof. by apply: (iffP flatten_mapP) => [][x Px]; exists x; rewrite ?mem_enum in Px *. Qed. -Arguments flatten_imageP [aT rT A P y]. +Arguments flatten_imageP {aT rT A P y}. Section CardFunImage. @@ -1253,7 +1252,7 @@ Qed. End CardFunImage. -Arguments image_injP [T T' f A]. +Arguments image_injP {T T' f A}. Section FinCancel. diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index 16709ee..1475d55 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -198,8 +198,7 @@ Notation QuotType Q m := (@QuotType_pack _ Q m). Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id) (at level 0, format "[ 'quotType' 'of' Q ]") : form_scope. -Arguments repr [T qT]. -Prenex Implicits repr. +Arguments repr {T qT}. (************************) (* Exporting the theory *) @@ -248,8 +247,7 @@ Notation piE := (@equal_toE _ _). Canonical equal_to_pi T (qT : quotType T) (x : T) := @EqualTo _ (\pi_qT x) (\pi x) (erefl _). -Arguments EqualTo [T x equal_val]. -Prenex Implicits EqualTo. +Arguments EqualTo {T x equal_val}. Section Morphism. @@ -276,12 +274,11 @@ Lemma pi_morph11 : \pi (h a) = hq (equal_val x). Proof. by rewrite !piE. Qed. End Morphism. -Arguments pi_morph1 [T qT f fq]. -Arguments pi_morph2 [T qT g gq]. -Arguments pi_mono1 [T U qT p pq]. -Arguments pi_mono2 [T U qT r rq]. -Arguments pi_morph11 [T U qT qU h hq]. -Prenex Implicits pi_morph1 pi_morph2 pi_mono1 pi_mono2 pi_morph11. +Arguments pi_morph1 {T qT f fq}. +Arguments pi_morph2 {T qT g gq}. +Arguments pi_mono1 {T U qT p pq}. +Arguments pi_mono2 {T U qT r rq}. +Arguments pi_morph11 {T U qT qU h hq}. Notation "{pi_ Q a }" := (equal_to (\pi_Q a)) : quotient_scope. Notation "{pi a }" := (equal_to (\pi a)) : quotient_scope. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 94873a8..dd67256 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -159,8 +159,7 @@ Qed. End Paths. -Arguments pathP [T e x p]. -Prenex Implicits pathP. +Arguments pathP {T e x p}. Section EqPath. @@ -687,10 +686,10 @@ Qed. End EqTrajectory. -Arguments fpathP [T f x p]. -Arguments loopingP [T f x n]. -Arguments trajectP [T f x n y]. -Prenex Implicits traject fpathP loopingP trajectP. +Arguments fpathP {T f x p}. +Arguments loopingP {T f x n}. +Arguments trajectP {T f x n y}. +Prenex Implicits traject. Section UniqCycle. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 4bbea2a..02064c3 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -349,9 +349,8 @@ case/primeP=> _ min_p d_neq1; apply: (iffP idP) => [/min_p|-> //]. by rewrite (negPf d_neq1) /= => /eqP. Qed. -Arguments primeP [p]. -Arguments primePn [n]. -Prenex Implicits primePn primeP. +Arguments primeP {p}. +Arguments primePn {n}. Lemma prime_gt1 p : prime p -> 1 < p. Proof. by case/primeP. Qed. @@ -541,8 +540,7 @@ exists (pdiv n); rewrite pdiv_dvd pdiv_prime //; split=> //. by case: leqP npr_p => //; move/ltn_pdiv2_prime->; auto. Qed. -Arguments primePns [n]. -Prenex Implicits primePns. +Arguments primePns {n}. Lemma pdivP n : n > 1 -> {p | prime p & p %| n}. Proof. by move=> lt1n; exists (pdiv n); rewrite ?pdiv_dvd ?pdiv_prime. Qed. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 9c13df3..ba1f969 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -786,12 +786,12 @@ End Sequences. Definition rev T (s : seq T) := nosimpl (catrev s [::]). -Arguments nilP [T s]. -Arguments all_filterP [T a s]. +Arguments nilP {T s}. +Arguments all_filterP {T a s}. -Prenex Implicits size nilP head ohead behead last rcons belast. +Prenex Implicits size head ohead behead last rcons belast. Prenex Implicits cat take drop rev rot rotr. -Prenex Implicits find count nth all has filter all_filterP. +Prenex Implicits find count nth all has filter. Notation count_mem x := (count (pred_of_simpl (pred1 x))). @@ -1354,10 +1354,9 @@ Proof. by elim: s n => [|y s' IHs] [|n] /=; auto. Qed. Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x). Proof. by case: s. Qed. -Arguments nthP [T s x]. -Arguments has_nthP [T a s]. -Arguments all_nthP [T a s]. -Prenex Implicits nthP has_nthP all_nthP. +Arguments nthP {T s x}. +Arguments has_nthP {T a s}. +Arguments all_nthP {T a s}. Definition bitseq := seq bool. Canonical bitseq_eqType := Eval hnf in [eqType of bitseq]. @@ -1598,10 +1597,10 @@ End PermSeq. Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2). Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2). -Arguments perm_eqP [T s1 s2]. -Arguments perm_eqlP [T s1 s2]. -Arguments perm_eqrP [T s1 s2]. -Prenex Implicits perm_eq perm_eqP perm_eqlP perm_eqrP. +Arguments perm_eqP {T s1 s2}. +Arguments perm_eqlP {T s1 s2}. +Arguments perm_eqrP {T s1 s2}. +Prenex Implicits perm_eq. Hint Resolve perm_eq_refl. Section RotrLemmas. @@ -1875,7 +1874,7 @@ Proof. by case/subseqP=> m _ -> Us2; apply: mask_uniq. Qed. End Subseq. Prenex Implicits subseq. -Arguments subseqP [T s1 s2]. +Arguments subseqP {T s1 s2}. Hint Resolve subseq_refl. @@ -2119,8 +2118,7 @@ Proof. by apply: map_inj_in_uniq; apply: in2W. Qed. End EqMap. -Arguments mapP [T1 T2 f s y]. -Prenex Implicits mapP. +Arguments mapP {T1 T2 f s y}. Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) : {f | uniq s -> size fs = size s -> map f s = fs}. @@ -2685,7 +2683,7 @@ elim: A => /= [|s A /iffP IH_A]; [by right; case | rewrite mem_cat]. have [s_x|s'x] := @idP (x \in s); first by left; exists s; rewrite ?mem_head. by apply: IH_A => [[t] | [t /predU1P[->|]]]; exists t; rewrite // mem_behead. Qed. -Arguments flattenP [A x]. +Arguments flattenP {A x}. Lemma flatten_mapP (A : S -> seq T) s y : reflect (exists2 x, x \in s & y \in A x) (y \in flatten (map A s)). @@ -2696,8 +2694,8 @@ Qed. End EqFlatten. -Arguments flattenP [T A x]. -Arguments flatten_mapP [S T A s y]. +Arguments flattenP {T A x}. +Arguments flatten_mapP {S T A s y}. Lemma perm_undup_count (T : eqType) (s : seq T) : perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 78d50b6..b24da11 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -394,7 +394,7 @@ apply: (iffP idP); last by elim: n / => // n _ /leq_trans->. elim: n => [|n IHn]; first by case: m. by rewrite leq_eqVlt ltnS => /predU1P[<- // | /IHn]; right. Qed. -Arguments leP [m n]. +Arguments leP {m n}. Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat. Proof. @@ -411,7 +411,7 @@ Qed. Lemma ltP m n : reflect (m < n)%coq_nat (m < n). Proof. exact leP. Qed. -Arguments ltP [m n]. +Arguments ltP {m n}. Lemma lt_irrelevance m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat. Proof. exact: (@le_irrelevance m.+1). Qed. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 38e3dbe..9154eb5 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -266,8 +266,8 @@ Proof. by rewrite -existsb_tnth; apply: existsP. Qed. End TupleQuantifiers. -Arguments all_tnthP [n T a t]. -Arguments has_tnthP [n T a t]. +Arguments all_tnthP {n T a t}. +Arguments has_tnthP {n T a t}. Section EqTuple. |