From 6c89f5de983e30964ff80029d801403ccd484a46 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 5 Jan 2013 02:01:55 +0100
Subject: [PATCH] Add missing notations on Z.

---
 theories/numbers.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/numbers.v b/theories/numbers.v
index 420bf690..c4198fef 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -88,6 +88,9 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%Z : Z_scope.
 Notation "(≤)" := Z.le (only parsing) : Z_scope.
 Notation "(<)" := Z.lt (only parsing) : Z_scope.
 
+Infix "`div`" := Z.div (at level 35) : Z_scope.
+Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
+
 Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
 Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y)%Z := Z_le_dec.
 Instance Z_lt_dec: ∀ x y : Z, Decision (x < y)%Z := Z_lt_dec.
-- 
GitLab