Merge pull request #27 from pi8027/fix-mathcomp-682

Fix w.r.t. math-comp/math-comp#682
coq-community · Jun 4, 2023 · f127f32 · f127f32
2 parents 3e39e52 + ef7070b
commit f127f32
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/realprop.v b/theories/realprop.v
@@ -690,7 +690,7 @@ Proof. by rewrite lez_addr1 ltNge; apply: (iffP idP) => /intR_leP. Qed.
 
 Lemma ratRE a : ratRR a == numq a / denq a.
 Proof.
-by rewrite /ratRR /ratR unfold_in/=; case: eqP => // ->; rewrite invR1 mulR1.
+by rewrite /ratRR /ratR Qint_def; case: eqP => // ->; rewrite invR1 mulR1.
 Qed.
 
 Lemma ratR_eq a : {r | a = (r.1%:Q / r.2.+1%:Q)%R & a * r.2.+1 == r.1}.