diff options
| author | Cyril Cohen | 2020-06-09 01:16:56 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-09 04:45:15 +0200 |
| commit | 8006cbf40eeb017aacb3ecaa8c4538f9a5aaa3bf (patch) | |
| tree | 805fe2e3ff31c9741ae0ded3cd7ab24b7068f60d /mathcomp/ssreflect/bigop.v | |
| parent | 6784363d60493b8ec154bbf1e827ec677d6b5921 (diff) | |
fix coq 8.12 warnings
Diffstat (limited to 'mathcomp/ssreflect/bigop.v')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 18 |
1 files changed, 6 insertions, 12 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index de03369..5f1b7d7 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -158,11 +158,9 @@ Reserved Notation "\sum_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \sum_ ( i | P ) '/ ' F ']'"). Reserved Notation "\sum_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). (* only parsing *) Reserved Notation "\sum_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). (* only parsing *) Reserved Notation "\sum_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \sum_ ( i < n | P ) '/ ' F ']'"). @@ -195,11 +193,9 @@ Reserved Notation "\max_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \max_ ( i | P ) '/ ' F ']'"). Reserved Notation "\max_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). (* only parsing *) Reserved Notation "\max_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). (* only parsing *) Reserved Notation "\max_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \max_ ( i < n | P ) '/ ' F ']'"). @@ -232,11 +228,9 @@ Reserved Notation "\prod_ ( i | P ) F" (at level 36, F at level 36, i at level 50, format "'[' \prod_ ( i | P ) '/ ' F ']'"). Reserved Notation "\prod_ ( i : t | P ) F" - (at level 36, F at level 36, i at level 50, - only parsing). + (at level 36, F at level 36, i at level 50). (* only parsing *) Reserved Notation "\prod_ ( i : t ) F" - (at level 36, F at level 36, i at level 50, - only parsing). + (at level 36, F at level 36, i at level 50). (* only parsing *) Reserved Notation "\prod_ ( i < n | P ) F" (at level 36, F at level 36, i, n at level 50, format "'[' \prod_ ( i < n | P ) '/ ' F ']'"). |