From 807faaddf00d75c365761a03e193baa2e40ac6df Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 12 Apr 2024 10:08:41 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18880

---
 model/Zmod/IrrCrit.v    | 4 ++--
 model/setoids/Nsetoid.v | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/model/Zmod/IrrCrit.v b/model/Zmod/IrrCrit.v
index 0aa4414c..e9fec357 100644
--- a/model/Zmod/IrrCrit.v
+++ b/model/Zmod/IrrCrit.v
@@ -51,8 +51,8 @@ polynomial is irreducible over the prime field Fp, then it is irreducible over
 Z.
 *)
 
-Variable p : positive.
-Hypothesis Hprime : (Prime p).
+Parameter p : positive.
+Axiom Hprime : (Prime p).
 
 Definition fp := (Fp p Hprime).
 
diff --git a/model/setoids/Nsetoid.v b/model/setoids/Nsetoid.v
index b78bdbda..ebb9b5e3 100644
--- a/model/setoids/Nsetoid.v
+++ b/model/setoids/Nsetoid.v
@@ -263,8 +263,7 @@ Proof.
  exact pfun3.
 Defined.
 
-
-Let ex_3_ary: (on 3 5 7 plus3)[=] 3+5+7.
+#[local] Lemma ex_3_ary: (on 3 5 7 plus3)[=] 3+5+7.
 Proof.
  simpl.
  reflexivity.