From 0b86e6b3f9620807659eddaa95a8a3dc074b811c Mon Sep 17 00:00:00 2001
From: Columbus240 <8899730+Columbus240@users.noreply.github.com>
Date: Sun, 10 Jan 2021 22:46:17 +0100
Subject: [PATCH] Patch for coq v8.10

---
 theories/Topology/EuclideanSpaces.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/theories/Topology/EuclideanSpaces.v b/theories/Topology/EuclideanSpaces.v
index 5ab27e1d..10b5eb5f 100644
--- a/theories/Topology/EuclideanSpaces.v
+++ b/theories/Topology/EuclideanSpaces.v
@@ -5,10 +5,12 @@
    Does every compact manifold (or topological-space (maybe Hausdorff is necessary)) admit a uniform probability distribution?
 *)
 
+Require Import FunctionalExtensionality.
+Require Import RTopology.
 Require Import Vector.
 Require Import ProductTopology.
-Require Import RTopology.
-Require Import FunctionalExtensionality.
+Require Import Ensembles.
+Require Import Compactness.
 
 (* Using [Fin.t] instead of repeated application of ProductTopology2 makes that we don’t have to consider associativity. Using [Vector] instead of [ProductTopology] makes that we don’t have to always consider functional extensionality. *)
 Definition FiniteProduct (A : TopologicalSpace) (n : nat) :=
@@ -145,7 +147,6 @@ Definition EuclideanSpace_scalarproduct {n : nat} (x y : point_set (EuclideanSpa
 
 Program Definition EuclideanSpace_scalarproduct_self_nonneg {n : nat} (x : point_set (EuclideanSpace n)) : nonnegreal :=
   {| nonneg := EuclideanSpace_scalarproduct x x; |}.
-Proof.
 Next Obligation.
   unfold EuclideanSpace_scalarproduct.
   induction x.