From 406f98b0efed0b5ed0c680c8a747b307d50c8ff4 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 20 Feb 2018 15:17:00 +0100 Subject: Remove the deprecation for some 8.2-8.5 compatibility aliases. This was decided during the Fall WG (2017). The aliases that are kept as deprecated are the ones where the difference is only a prefix becoming a qualified module name. The intention is to turn the warning for deprecated notations on. We change the compat version to 8.6 to allow the removal of VOld and V8_5. --- theories/QArith/Qreduction.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/QArith') diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 5d055b547..959a7e5bd 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -11,8 +11,8 @@ Require Export QArith_base. Require Import Znumtheory. -Notation Z2P := Z.to_pos (compat "8.3"). -Notation Z2P_correct := Z2Pos.id (compat "8.3"). +Notation Z2P := Z.to_pos (only parsing). +Notation Z2P_correct := Z2Pos.id (only parsing). (** Simplification of fractions using [Z.gcd]. This version can compute within Coq. *) -- cgit v1.2.3