Move `sprop` file to `base` and improve documentation.

README.md

@@ -40,6 +40,9 @@ Notably:
   [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
   becomes unreliable. We do not consider this an issue since we use `lia` (for
   which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
+* `Set Allow StrictProp`: the type of strict propositions (`SProp`) is enabled
+  by default since Coq 8.12. To make prior versions of Coq happy we need to
+  allow it explicitly.
 
 ## Prerequisites
 

_CoqProject

@@ -5,7 +5,6 @@
 theories/options.v
 theories/base.v
 theories/tactics.v
-theories/sprop.v
 theories/option.v
 theories/fin_map_dom.v
 theories/boolset.v

theories/base.v

@@ -10,6 +10,7 @@ we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
 over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
 From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
+From Coq Require Export Logic.StrictProp.
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 From stdpp Require Import options.
@@ -49,6 +50,10 @@ Obligation Tactic := idtac.
 (** 3. Hide obligations from the results of the [Search] commands. *)
 Add Search Blacklist "_obligation_".
 
+(** 4. [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.
+
 (** * Sealing off definitions *)
 Section seal.
   Local Set Primitive Projections.
@@ -645,6 +650,21 @@ Proof. destruct b; simpl; tauto. Qed.
 Lemma Is_true_false (b : bool) : b = false → ¬b.
 Proof. now intros -> ?. Qed.
 
+(** ** SProp *)
+Lemma unsquash (P : Prop) `{!Decision P} : Squash P → P.
+Proof.
+  intros HP. destruct (decide P) as [?|HnotP]; [assumption|].
+  assert sEmpty as []. destruct HP. destruct HnotP; assumption.
+Qed.
+
+Definition SIs_true (b : bool) : SProp := Squash (Is_true b).
+
+Lemma SIs_true_intro b : Is_true b → SIs_true b.
+Proof. apply squash. Qed.
+Lemma SIs_true_elim b : SIs_true b → Is_true b.
+Proof. apply unsquash. destruct b; [left|right]; simpl; tauto. Qed.
+
+
 (** ** Unit *)
 Global Instance unit_equiv : Equiv unit := λ _ _, True.
 Global Instance unit_equivalence : Equivalence (≡@{unit}).

theories/numbers.v

@@ -3,7 +3,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful
 notations. *)
 From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
-From stdpp Require Export base decidable option sprop.
+From stdpp Require Export base decidable option.
 From stdpp Require Import options.
 Local Open Scope nat_scope.
 

theories/pmap.v

@@ -8,7 +8,6 @@ Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
 From stdpp Require Import mapset countable.
 From stdpp Require Export fin_maps.
-From stdpp Require Export sprop.
 From stdpp Require Import options.
 
 Local Open Scope positive_scope.

theories/sprop.v

-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.
-Proof.
-  intros HP. destruct (decide P) as [?|HnotP]; [assumption|].
-  assert sEmpty as []. destruct HP. destruct HnotP; assumption.
-Qed.
-
-Definition SIs_true (b : bool) : SProp := Squash (Is_true b).
-
-Lemma SIs_true_intro b : Is_true b → SIs_true b.
-Proof. apply squash. Qed.
-Lemma SIs_true_elim b : SIs_true b → Is_true b.
-Proof. apply (unsquash _). Qed.