Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/21947 #1265

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

Merged
ppedrot merged 1 commit into from
May 26, 2026
Merged

Adapt to https://github.com/rocq-prover/rocq/pull/21947 #1265

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
1 change: 1 addition & 0 deletions erasure/theories/ECoInductiveToInductive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ Import MRList (map_InP, map_InP_elim, map_InP_spec).

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EConstructorsAsBlocks.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EAriti

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EEtaExpanded.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EGloba

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EEtaExpandedFix.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,6 +213,7 @@ Qed.

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EGenericGlobalMap.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ From MetaRocq.Erasure Require Import EAst EAstUtils EInduction EArities

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EGenericMapEnv.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ From MetaRocq.Erasure Require Import EAst EAstUtils EInduction EArities

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EImplementBox.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EAriti

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EInlineProjections.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EExtends

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EOptimizePropDiscr.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EDeps EExtends

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/ERemoveParams.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EAriti

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EUnboxing.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EAriti

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction ELiftS
EWellformed ECSubst EInduction EWcbvEvalInd EEtaExpanded.

Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
From Equations Require Import Equations.
Set Equations Transparent.
Local Set Keyed Unification.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction ELiftS
EWellformed ECSubst EInduction EWcbvEvalInd EEtaExpanded.

Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
From Equations Require Import Equations.
Set Equations Transparent.
Local Set Keyed Unification.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EWcbvEvalEtaInd.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EWcbvE
EWellformed ECSubst EInduction EWcbvEvalInd EEtaExpanded.

Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
From Equations Require Import Equations.
Set Equations Transparent.
Local Set Keyed Unification.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EWcbvEvalInd.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ From MetaRocq.Common Require Import config Kernames BasicAst EnvMap.
From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EWcbvEval EGlobalEnv ECSubst EInduction.

Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
From Equations Require Import Equations.
Set Equations Transparent.
Local Set Keyed Unification.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/EWellformed.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ From MetaRocq.PCUIC Require Import PCUICTactics.

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/ErasureFunction.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAstUtils ELiftSubst EArities Ex

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Local Set Keyed Unification.
Set Default Proof Using "Type*".
Import MonadNotation.
Expand Down
1 change: 1 addition & 0 deletions erasure/theories/ErasureFunctionProperties.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAstUtils ELiftSubst EArities Ex

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Local Set Keyed Unification.
Set Default Proof Using "Type*".
Import MonadNotation.
Expand Down
1 change: 1 addition & 0 deletions pcuic/theories/Bidirectional/BDTyping.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ From MetaRocq.PCUIC Require Import PCUICAst PCUICAstUtils
From MetaRocq.Utils Require Export LibHypsNaming.
From Stdlib Require Import ssreflect.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
From Equations.Type Require Import Relation.
From Equations.Prop Require Import DepElim.
From Equations Require Import Equations.
Expand Down
1 change: 1 addition & 0 deletions pcuic/theories/PCUICNormal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ From MetaRocq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICOnOn
PCUICInduction PCUICRedTypeIrrelevance PCUICOnFreeVars PCUICEtaExpand.
From Stdlib Require Import ssreflect ssrbool.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

(* Require Import Equations.Type.DepElim. *)

Expand Down
1 change: 1 addition & 0 deletions pcuic/theories/Syntax/PCUICInduction.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ From Equations Require Import Equations.
From Equations.Prop Require Import Subterm.

Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import PCUICEnvTyping.

(** Derive the well-founded subterm relation for terms. Not so useful
Expand Down
1 change: 1 addition & 0 deletions safechecker/theories/PCUICSafeRetyping.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ Transparent Acc_intro_generator.

Local Open Scope string_scope.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Import MonadNotation.

#[global]
Expand Down
1 change: 1 addition & 0 deletions utils/theories/utils.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ From Stdlib Require Export Bool ZArith Arith Lia List.
From MetaRocq.Utils Require Export MRUtils monad_utils.

Global Set Asymmetric Patterns.
#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.

@SkySkimmer SkySkimmer May 18, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we really shouldn't use global

@SkySkimmer SkySkimmer May 26, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this one is fine because Set Asymmetric Patterns above is also global but the others should probably match their Set Asymmetric Patterns


Global Open Scope bs_scope.

Expand Down
Loading