diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 10:05:49 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 10:05:49 +0100 |
commit | 35aa5686aa5352dfdb62002db56720c1d3e144ce (patch) | |
tree | c17f1b86335ce15766555bb468025b93c0e26ffc /plugins/setoid_ring | |
parent | 5213bcdfd2baa5e2e652eaa63fff8d3268959489 (diff) | |
parent | 4a7d2e906c79fcae452d44ec12de8037d2843fbc (diff) |
Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v)
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 776ebd808..14aead045 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -263,7 +263,7 @@ Section ALMOST_RING. Variable SRth : semi_ring_theory 0 1 radd rmul req. (** Every semi ring can be seen as an almost ring, by taking : - -x = x and x - y = x + y *) + [-x = x] and [x - y = x + y] *) Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). Definition SRsub x y := x + -y. Infix "-" := SRsub. |