From 4a7d2e906c79fcae452d44ec12de8037d2843fbc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 20 Feb 2018 14:35:54 +0100
Subject: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in
 Ring_theory.v).

---
 plugins/setoid_ring/Ring_theory.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 776ebd808d..14aead0452 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.
-- 
cgit v1.2.3