From c1473ea9215961649479075f1b6ac3690a593011 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 22 Feb 2017 14:17:09 +0100
Subject: [PATCH] Remove some notations that are already in the Coq stdlib.

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

diff --git a/theories/numbers.v b/theories/numbers.v
index d066c13a..4e27271a 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -25,7 +25,6 @@ Reserved Notation "x ≤ y ≤ z ≤ z'"
 Infix "≤" := le : nat_scope.
 Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%nat : nat_scope.
 Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%nat : nat_scope.
-Notation "x < y < z" := (x < y ∧ y < z)%nat : nat_scope.
 Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%nat : nat_scope.
 Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_scope.
 Notation "(≤)" := le (only parsing) : nat_scope.
@@ -106,7 +105,6 @@ Open Scope positive_scope.
 Infix "≤" := Pos.le : positive_scope.
 Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) : positive_scope.
 Notation "x ≤ y < z" := (x ≤ y ∧ y < z) : positive_scope.
-Notation "x < y < z" := (x < y ∧ y < z) : positive_scope.
 Notation "x < y ≤ z" := (x < y ∧ y ≤ z) : positive_scope.
 Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : positive_scope.
 Notation "(≤)" := Pos.le (only parsing) : positive_scope.
@@ -186,7 +184,6 @@ Close Scope positive_scope.
 Infix "≤" := N.le : N_scope.
 Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%N : N_scope.
 Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%N : N_scope.
-Notation "x < y < z" := (x < y ∧ y < z)%N : N_scope.
 Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
 Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope.
 Notation "(≤)" := N.le (only parsing) : N_scope.
-- 
GitLab