From 4d521764d1062a10f108086cc1bde4ba62e16b08 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Mon, 7 Jun 2021 13:19:30 +0200
Subject: Port the Coq part

---
 src/classes/SMT_classes.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/classes/SMT_classes.v')

diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
index 49729db..be16138 100644
--- a/src/classes/SMT_classes.v
+++ b/src/classes/SMT_classes.v
@@ -98,6 +98,8 @@ Class OrdType T := {
   lt_not_eq : forall x y : T, lt x y -> x <> y
 }.
 
+#[export] Hint Resolve lt_not_eq lt_trans : typeclass_ordtype.
+
 
 Global Instance StrictOrder_OrdType T `(OrdType T) :
   StrictOrder (lt : T -> T -> Prop).
@@ -182,7 +184,7 @@ Proof.
   intros x y. destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE.
 Qed.
 
-Hint Resolve
+#[export] Hint Resolve
      ord_of_compdec
      inh_of_compdec
      comp_of_compdec
-- 
cgit