From 0a0bd5d2881f547fdda6f81636424ad4b9c74c32 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Mar 2019 17:22:38 +0100
Subject: [PATCH] Ensure that `Nat.max` only `simpl`s if it does not result
 into a pattern match.

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

diff --git a/theories/numbers.v b/theories/numbers.v
index 2455887c..80dc45a1 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -15,6 +15,8 @@ Proof. solve_decision. Defined.
 
 (** * Notations and properties of [nat] *)
 Arguments minus !_ !_ / : assert.
+Arguments Nat.max : simpl nomatch.
+
 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