From 462ea92aebba670fc4ad47b535390d5932fe384a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 20 Sep 2015 14:35:57 +0200
Subject: [PATCH] Misc prelude omissions.

---
 theories/base.v    | 3 +++
 theories/numbers.v | 1 +
 2 files changed, 4 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 82c6b8d6..24ea3864 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -862,6 +862,9 @@ Instance idem_propholds {A} (R : relation A) f :
   Idempotent R f → ∀ x, PropHolds (R (f x x) x).
 Proof. red. trivial. Qed.
 
+Instance: ∀ `{R1 : relation A, R2 : relation B} (x : B),
+  Reflexive R2 → Proper (R1 ==> R2) (λ _, x).
+Proof. intros A R1 B R2 x ? y1 y2; reflexivity. Qed.
 Instance: @PreOrder A (=).
 Proof. split; repeat intro; congruence. Qed.
 Lemma injective_iff {A B} {R : relation A} {S : relation B} (f : A → B)
diff --git a/theories/numbers.v b/theories/numbers.v
index f0f366a8..d7d5ec96 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -11,6 +11,7 @@ Open Scope nat_scope.
 Coercion Z.of_nat : nat >-> Z.
 
 (** * Notations and properties of [nat] *)
+Arguments minus !_ !_ /.
 Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
 Reserved Notation "x ≤ y < z" (at level 70, y at next level).
 Reserved Notation "x < y < z" (at level 70, y at next level).
-- 
GitLab