From 05751ed0757aa9a83dee2bbd28345a9d8929c674 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 1 Apr 2026 15:28:10 +0200 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21849 --- theories/PFsection3.v | 6 +++--- theories/PFsection4.v | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/PFsection3.v b/theories/PFsection3.v index 38f712a..60fb341 100644 --- a/theories/PFsection3.v +++ b/theories/PFsection3.v @@ -203,10 +203,10 @@ Definition AndLit kvs kv := kv :: kvs. Definition AddLit := AndLit. Declare Scope defclause_scope. Notation "(*dummy*)" := (Prop Prop) : defclause_scope. -Arguments AddLit _%defclause_scope _. +Arguments AddLit _%_defclause_scope _. Infix "+" := AddLit : defclause_scope. Definition SubLit kvs kv := AddLit kvs (kv.1, - kv.2). -Arguments SubLit _%defclause_scope _. +Arguments SubLit _%_defclause_scope _. Infix "-" := SubLit : defclause_scope. Coercion LastLit kv := [:: kv]. @@ -223,7 +223,7 @@ Notation "& kv1 , .. , kvn 'in' ij" := Notation "& ? 'in' ij" := (Clause ij nil) (at level 200, ij at level 0, format "& ? 'in' ij"). Definition DefClause := Clause. -Arguments DefClause _ _%defclause_scope. +Arguments DefClause _ _%_defclause_scope. Notation "& ij = kvs" := (DefClause ij kvs) (at level 200, ij at level 0, format "& ij = kvs"). diff --git a/theories/PFsection4.v b/theories/PFsection4.v index 268688a..1a0b45f 100644 --- a/theories/PFsection4.v +++ b/theories/PFsection4.v @@ -148,7 +148,7 @@ Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) & W1 \x W2 = W := End Four_1_to_2. -Arguments primeTI_hypothesis _ _%g _%g _%g _ _%g _%g. +Arguments primeTI_hypothesis _ _%_g _%_g _%_g _ _%_g _%_g. Section Four_3_to_5.