From d61ed9a87f7852f2b7fa8057cffe912c73cd5f93 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 8 Mar 2018 10:44:38 +0100 Subject: [PATCH] Get rid of some deprecated notations. --- theories/countable.v | 4 ++-- theories/numbers.v | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/countable.v b/theories/countable.v index de849d7..567903a 100644 --- a/theories/countable.v +++ b/theories/countable.v @@ -37,9 +37,9 @@ Section choice. Context `{Countable A} (P : A → Prop). Inductive choose_step: relation positive := - | choose_step_None {p} : decode (A:=A) p = None → choose_step (Psucc p) p + | choose_step_None {p} : decode (A:=A) p = None → choose_step (Pos.succ p) p | choose_step_Some {p} {x : A} : - decode p = Some x → ¬P x → choose_step (Psucc p) p. + decode p = Some x → ¬P x → choose_step (Pos.succ p) p. Lemma choose_step_acc : (∃ x, P x) → Acc choose_step 1%positive. Proof. intros [x Hx]. cut (∀ i p, diff --git a/theories/numbers.v b/theories/numbers.v index dff4886..78bb1b5 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -223,10 +223,10 @@ Proof. by injection 1. Qed. Instance N_eq_dec: EqDecision N := N.eq_dec. Program Instance N_le_dec : RelDecision N.le := λ x y, - match Ncompare x y with Gt => right _ | _ => left _ end. + match N.compare x y with Gt => right _ | _ => left _ end. Solve Obligations with naive_solver. Program Instance N_lt_dec : RelDecision N.lt := λ x y, - match Ncompare x y with Lt => left _ | _ => right _ end. + match N.compare x y with Lt => left _ | _ => right _ end. Solve Obligations with naive_solver. Instance N_inhabited: Inhabited N := populate 1%N. Instance N_le_po: PartialOrder (≤)%N. -- 2.26.2