From ab2f61dd595597e70aed17a8964f1bec9817686e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 07:20:34 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 theories/numbers.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/numbers.v b/theories/numbers.v
index 0824477f..13e32b54 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -724,7 +724,7 @@ Local Close Scope Qc_scope.
 (** We define the type [Qp] of positive rationals as fractions of positives with
 an [SProp]-based proof that ensures the fraction is in canonical form (i.e., its
 gcd is 1). Note that we do not define [Qp] as a subset (i.e., Sigma) of the
-standard library's [Qc]. The type [Qc] uses a [Prop]-based proof for canonicity
+standard library's [Qc] because the type [Qc] uses a [Prop]-based proof (not [SProp]) for canonicity
 of the fraction. *)
 Definition Qp_red (q : positive * positive) : positive * positive :=
   (Pos.ggcd (q.1) (q.2)).2.
-- 
GitLab