Merge pull request #1132 from SkySkimmer/classify-warn

Adapt to coq/coq#19981 (Set Warnings is synterp phase)

quotation/theories/ToPCUIC/Init.v

@@ -1,3 +1,4 @@
+Set Warnings "-notation-overridden".
 From MetaCoq.Utils Require Export bytestring.
 From MetaCoq.Utils Require Import utils MCList.
 From MetaCoq.Common Require Import MonadBasicAst.
@@ -9,6 +10,8 @@ Require Import Stdlib.Lists.List.
 Export TemplateMonad.Common (export, local, global).
 Import ListNotations.
 
+Set Warnings "+notation-overridden".
+
 Local Set Primitive Projections.
 Local Unset Universe Minimization ToSet.
 Local Open Scope bs.

template-pcuic/metacoq-config

@@ -1,2 +1,2 @@
 # DO NOT EDIT THIS FILE: autogenerated from ./configure.sh
-
+-R ../utils/theories MetaCoq.Utils -R ../common/theories MetaCoq.Common -R ../pcuic/theories MetaCoq.PCUIC -R ../template-coq/theories MetaCoq.Template -I ../template-coq

template-pcuic/theories/Loader.v

@@ -7,7 +7,7 @@ From MetaCoq.TemplatePCUIC Require Import TemplateMonadToPCUIC.
 Notation eval_pcuic_quotation := eval_pcuic_quotation (only parsing).
 #[export] Existing Instance default_eval_pcuic_quotation.
 
-#[export] Set Warnings "-notation-overridden".
+Set Warnings "-notation-overridden".
 (* Work around COQBUG(https://github.com/coq/coq/issues/16715) *)
 Notation "<% x %>" := (match @monad_trans return _ with monad_trans => ltac:(let monad_trans := constr:(monad_trans _) in let p y := exact y in let p y := run_template_program (monad_trans y) p in quote_term x p) end)
   (only parsing).
@@ -16,4 +16,3 @@ Notation "<% x %>" := (match @monad_trans return _ with monad_trans => ltac:(let
 (* Use [return _] to avoid running the program twice on failure *)
 Notation "<# x #>" := (match @PCUICTemplateMonad.Core.tmQuoteRec return _ with tmQuoteRec => ltac:(let qx := constr:(tmQuoteRec _ _ x) in let p y := exact y in run_template_program qx p) end)
   (only parsing).
-#[export] Set Warnings "+notation-overridden".