diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-09-28 17:49:41 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-09-28 17:49:41 +0200 |
| commit | ed53e048fc5e4b995c1e0c42bf1ba1611c331cce (patch) | |
| tree | de30a57d59a332cf895724ad6a28d68601f6c51c /plugins/setoid_ring | |
| parent | 1c3bc5642fe29855cc4d72aa677ff7ffd4787271 (diff) | |
Ring_theory: avoid overriding a few notations
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 7fcd6c08a..f7757a18d 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -238,7 +238,6 @@ Section ALMOST_RING. Variable req : R -> R -> Prop. Notation "0" := rO. Notation "1" := rI. Infix "==" := req. Infix "+" := radd. Infix "* " := rmul. - Infix "-" := rsub. Notation "- x" := (ropp x). (** Leibniz equality leads to a setoid theory and is extensional*) Lemma Eqsth : Equivalence (@eq R). @@ -263,7 +262,7 @@ Section ALMOST_RING. -x = x and x - y = x + y *) Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). - Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). + Definition SRsub x y := x + -y. Infix "-" := SRsub. Lemma SRopp_ext : forall x y, x == y -> -x == -y. Proof. intros x y H; exact H. Qed. @@ -320,6 +319,8 @@ Section ALMOST_RING. Qed. End SEMI_RING. + Infix "-" := rsub. + Notation "- x" := (ropp x). Variable Reqe : ring_eq_ext radd rmul ropp req. Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. |