diff --git a/theories/numbers.v b/theories/numbers.v
index 253a48971b2b476db3802095358072eda5a7c4c4..0824477f665e2279abcd3439b1d2620934244dc3 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -721,6 +721,11 @@ Qed.
 Local Close Scope Qc_scope.
 
 (** * Positive rationals *)
+(** 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
+of the fraction. *)
 Definition Qp_red (q : positive * positive) : positive * positive :=
   (Pos.ggcd (q.1) (q.2)).2.
 Definition Qp_wf (q : positive * positive) : SProp :=
diff --git a/theories/sprop.v b/theories/sprop.v
index 1e6a0be06386f1109718477edd0054a2805601e0..f2c68709cab620272e29b568196722d24029dafd 100644
--- a/theories/sprop.v
+++ b/theories/sprop.v
@@ -2,6 +2,8 @@ From Coq Require Export Logic.StrictProp.
 From stdpp Require Import decidable.
 From stdpp Require Import options.
 
+(** [StrictProp] is enabled by default since Coq 8.12. To make prior versions
+of Coq happy we need to allow it explicitly. *)
 Global Set Allow StrictProp.
 
 Lemma unsquash (P : Prop) `{!Decision P} : Squash P → P.