Adapt to coq/coq#18880

coq-community · Apr 12, 2024 · 807faad · 807faad
1 parent bdb702d
commit 807faad
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git 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
@@ -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.