From ad2f0a9366fbe3d49fd4cb822098f239cce967cf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Jul 2021 23:57:12 +0200
Subject: [PATCH] Comments.

---
 theories/numbers.v | 5 +++++
 theories/sprop.v   | 2 ++
 2 files changed, 7 insertions(+)

diff --git a/theories/numbers.v b/theories/numbers.v
index 253a4897..0824477f 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 1e6a0be0..f2c68709 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.
-- 
GitLab