Merge pull request HoTT#1863 from Alizter/ps/branch/surpress_argument…

…_scope_delimiter_warning surpress argument-scope-delimiter warning
Alizter · Feb 19, 2024 · 2673d0f · 2673d0f
2 parents 70bce19 + 5f83697
commit 2673d0f
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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. *)