diff options
| author | Enrico Tassi | 2020-01-21 07:49:42 +0100 |
|---|---|---|
| committer | GitHub | 2020-01-21 07:49:42 +0100 |
| commit | d3f5e11aa1bbdf6ee4a111bf4641d162d289340f (patch) | |
| tree | cfbffa5bcb66e1eb27c14eb79c1aea01fe3b758f /mathcomp/ssreflect | |
| parent | 2646a263ba499f50ad09816ef76bea683517da26 (diff) | |
| parent | faa2b32bac7454bcec366d9790b6f14331e297b0 (diff) | |
Merge pull request #452 from SimonBoulier/non_maximal_implicit
Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 53a933a..6d18825 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1662,8 +1662,8 @@ Arguments big_enum_val [R idx op I A] F. Arguments big_enum_rank [R idx op I A x] xA F. Arguments pair_big_dep [R idx op I J]. Arguments pair_big [R idx op I J]. -Arguments big_allpairs_dep [R idx op I1 I2 J h r1 r2 F]. -Arguments big_allpairs [R idx op I1 I2 r1 r2 F]. +Arguments big_allpairs_dep {R idx op I1 I2 J h r1 r2 F}. +Arguments big_allpairs {R idx op I1 I2 r1 r2 F}. Arguments exchange_big_dep [R idx op I J rI rJ P Q] xQ [F]. Arguments exchange_big_dep_nat [R idx op m1 n1 m2 n2 P Q] xQ [F]. Arguments big_ord_recl [R idx op]. |