diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 14:35:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 14:35:54 +0100 |
| commit | 4a7d2e906c79fcae452d44ec12de8037d2843fbc (patch) | |
| tree | 8e56db27d245da82542d94b6df3eec24587a8e78 /plugins/setoid_ring | |
| parent | aec63ba9c8f6840d98ba731640a786138d836343 (diff) | |
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. |