From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- lib/Decidableplus.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/Decidableplus.v') diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 6383794d..66dffb3a 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -86,10 +86,10 @@ Next Obligation. Qed. Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := { - Decidable_witness := beq_nat x y + Decidable_witness := Nat.eqb x y }. Next Obligation. - apply beq_nat_true_iff. + apply Nat.eqb_eq. Qed. Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := { -- cgit