aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-06-08 17:41:43 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-06-08 17:41:43 +0200
commita526ef890f614e130a8afc032d427c81fd8e6442 (patch)
tree99153f2ca1debe20f5954d7786de69436d50a102
parent102d7418e399de646b069924277e4baea1badaca (diff)
Fix bug 5026 (the stdlib shouldn't define inconsistent notations).
-rw-r--r--theories/QArith/Qcabs.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/QArith/Qcabs.v b/theories/QArith/Qcabs.v
index c0ababfff..e433ecffa 100644
--- a/theories/QArith/Qcabs.v
+++ b/theories/QArith/Qcabs.v
@@ -22,7 +22,7 @@ Lemma Qcabs_canon (x : Q) : Qred x = x -> Qred (Qabs x) = Qabs x.
Proof. intros H; now rewrite (Qred_abs x), H. Qed.
Definition Qcabs (x:Qc) : Qc := {| canon := Qcabs_canon x (canon x) |}.
-Notation "[ q ]" := (Qcabs q) (q at next level, format "[ q ]") : Qc_scope.
+Notation "[ q ]" := (Qcabs q) : Qc_scope.
Ltac Qc_unfolds :=
unfold Qcabs, Qcminus, Qcopp, Qcplus, Qcmult, Qcle, Q2Qc, this.