Adapt w.r.t. coq/coq#18895.

mit-plv · Apr 11, 2024 · 208894a · 208894a
1 parent 2a0a2c3
commit 208894a
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/RatUtil.v b/src/RatUtil.v
@@ -5,11 +5,11 @@ Create HintDb rat discriminated.
 Create HintDb ratsimpl discriminated.
 
 #[global]
-Hint Immediate (@reflexivity Rat eqRat _) : rat.
+Hint Extern 1 => simple eapply (@reflexivity Rat eqRat _) : rat.
 #[global]
-Hint Immediate (@reflexivity Rat leRat _) : rat.
+Hint Extern 1 => simple eapply (@reflexivity Rat leRat _) : rat.
 #[global]
-Hint Immediate (rat0_le_all) : rat.
+Hint Immediate rat0_le_all : rat.
 
 Lemma maxRat_same r : maxRat r r = r.
 Proof. intros; cbv [maxRat]; destruct (bleRat r r) eqn:?; trivial. Qed.