From 1c80ebf3e6c55b55ece323ccafef4e8e45e10a01 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 21 Sep 2024 19:21:33 +0200 Subject: [PATCH] silence "From Coq" warning Signed-off-by: Ali Caglayan --- contrib/SetoidRewrite.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/contrib/SetoidRewrite.v b/contrib/SetoidRewrite.v index d2bb4d7ad4e..94e0383652c 100644 --- a/contrib/SetoidRewrite.v +++ b/contrib/SetoidRewrite.v @@ -10,9 +10,11 @@ All files that import WildCat/SetoidRewrite.v will also recursively import the e (** Because of this, this file needs to be the *first* file Require'd in any file that uses it. Otherwise, the typeclasses hintdb is cleared, breaking typeclass inference. Moreover, if Foo Requires this file, then Foo must also be the first file Require'd in any file that Requires Foo, and so on. In the long term it would be good if this could be avoided.*) +#[warnings="deprecated"] From Coq Require Init.Tactics. From HoTT Require Import Basics.Overture Basics.Tactics. From HoTT Require Import Types.Forall. +#[warnings="deprecated"] From Coq Require Setoids.Setoid. Import CMorphisms.ProperNotations. From HoTT Require Import WildCat.Core