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/generic_quotient.v | |
| parent | 6784363d60493b8ec154bbf1e827ec677d6b5921 (diff) | |
fix coq 8.12 warnings
Diffstat (limited to 'mathcomp/ssreflect/generic_quotient.v')
| -rw-r--r-- | mathcomp/ssreflect/generic_quotient.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index 5ec4037..c8b1490 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -101,8 +101,8 @@ Reserved Notation "x != y %[mod_eq e ]" (at level 70, y at next level, no associativity, format "'[hv ' x '/' != y '/' %[mod_eq e ] ']'"). Reserved Notation "x <> y %[mod_eq e ]" (at level 70, y at next level, no associativity, format "'[hv ' x '/' <> y '/' %[mod_eq e ] ']'"). -Reserved Notation "{eq_quot e }" (at level 0, e at level 0, - format "{eq_quot e }", only parsing). +Reserved Notation "{eq_quot e }" + (at level 0, e at level 0, format "{eq_quot e }"). Delimit Scope quotient_scope with qT. Local Open Scope quotient_scope. |