From b48d40e92e8f8b6d7fbbb518cab6a5bbae5252a3 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 4 Jun 2021 13:04:20 +0200 Subject: [PATCH] Use `!` instead of `+`. --- theories/base.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/base.v b/theories/base.v index 13209d04..df49b47d 100644 --- a/theories/base.v +++ b/theories/base.v @@ -465,13 +465,13 @@ Class PartialOrder {A} (R : relation A) : Prop := { partial_order_pre :> PreOrder R; partial_order_anti_symm :> AntiSymm (=) R }. -Global Hint Mode PartialOrder ! + : typeclass_instances. +Global Hint Mode PartialOrder ! ! : typeclass_instances. Class TotalOrder {A} (R : relation A) : Prop := { total_order_partial :> PartialOrder R; total_order_trichotomy :> Trichotomy (strict R) }. -Global Hint Mode TotalOrder ! + : typeclass_instances. +Global Hint Mode TotalOrder ! ! : typeclass_instances. (** * Logic *) Global Instance prop_inhabited : Inhabited Prop := populate True. -- GitLab