Commit 0a0bd5d2 authored by Robbert Krebbers's avatar Robbert Krebbers

Ensure that `Nat.max` only `simpl`s if it does not result into a pattern match.

parent fa8a02f2
Pipeline #15127 passed with stage
in 8 minutes and 22 seconds
...@@ -15,6 +15,8 @@ Proof. solve_decision. Defined. ...@@ -15,6 +15,8 @@ Proof. solve_decision. Defined.
(** * Notations and properties of [nat] *) (** * Notations and properties of [nat] *)
Arguments minus !_ !_ / : assert. 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). 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).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment