From 5f836978257c4b5ce0ff52b0916381b64768794d Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 19 Feb 2024 02:51:07 +0000 Subject: [PATCH] surpress argument-scope-delimiter warning Signed-off-by: Ali Caglayan --- theories/Basics/Overture.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index 5d7d7d4ae65..9ba73df8f43 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -15,6 +15,9 @@ Create HintDb typeclass_instances discriminated. Local Set Polymorphic Inductive Cumulativity. +(** Disable warning about argument scope delimiters. TODO: remove this once we bump the minimal Coq version to 8.19 and merge #1862. *) +Global Set Warnings "-argument-scope-delimiter". + (** ** Type classes *) (** This command prevents Coq from trying to guess the values of existential variables while doing typeclass resolution. If you don't know what that means, ignore it. *)