From 6f737edae4b7e6243a9f11e74614f55381f62ec7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 2 Aug 2019 10:41:29 +0200 Subject: Coq 8.10 compatibility: make explicit the "core" hint database "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core". --- lib/Floats.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/Floats.v') diff --git a/lib/Floats.v b/lib/Floats.v index 7677e3c8..13350dd0 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -139,8 +139,8 @@ Definition default_nan_32 := quiet_nan_32 Archi.default_nan_32. Local Notation __ := (eq_refl Datatypes.Lt). -Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt). -Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt). +Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt) : core. +Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt) : core. (** * Double-precision FP numbers *) -- cgit