Comments.

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 :=

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.