Merge pull request #205 from coq-community/coq_18880

Adapt to coq/coq#18880
coq-community · Apr 12, 2024 · c30c93a · c30c93a
2 parents bdb702d + 807faad
commit c30c93a
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.