Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 1 commit into from
Jan 9, 2025
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions quotation/theories/ToPCUIC/Init.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand All @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion template-pcuic/metacoq-config
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
3 changes: 1 addition & 2 deletions template-pcuic/theories/Loader.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand All @@ -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".
Loading