From a526ef890f614e130a8afc032d427c81fd8e6442 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 8 Jun 2017 17:41:43 +0200 Subject: Fix bug 5026 (the stdlib shouldn't define inconsistent notations). --- theories/QArith/Qcabs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories') 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. -- cgit v1.2.3