From 8bd02d0f25971af69e22510e36fd0119d1283a47 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Feb 2015 18:30:40 +0100
Subject: [PATCH] compile again

---
 lib/ModuRes/CBUltInst.v  |  4 ++--
 lib/ModuRes/Constr.v     | 13 ++-----------
 lib/ModuRes/MetricCore.v |  8 ++++++++
 3 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/lib/ModuRes/CBUltInst.v b/lib/ModuRes/CBUltInst.v
index b3547d422..c1f896f7e 100644
--- a/lib/ModuRes/CBUltInst.v
+++ b/lib/ModuRes/CBUltInst.v
@@ -1,8 +1,8 @@
 (** This file provides the proof that CBUlt, the category of complete,
     bisected, ultrametric spaces, forms an M-category. *)
 
-Require Import MetricCore.
-Require Import MetricRec.
+Require Import CSetoid Constr.
+Require Import MetricCore MetricRec.
 
 Module CBUlt <: MCat.
   Local Open Scope cat_scope.
diff --git a/lib/ModuRes/Constr.v b/lib/ModuRes/Constr.v
index 5c3845a87..c6dce1e85 100644
--- a/lib/ModuRes/Constr.v
+++ b/lib/ModuRes/Constr.v
@@ -6,16 +6,9 @@
     - an extension operation on the space Tᵏ, for k ∈ nat, as a
       non-expansive morphism. *)
 
-Require Export UPred.
+Require Import UPred.
 Require Import MetricCore.
-Require Import Arith.
-
-Module NatDec.
-  Definition U := nat.
-  Definition eq_dec := eq_nat_dec.
-End NatDec.
-
-Module D := Coq.Logic.Eqdep_dec.DecidableEqDep(NatDec).
+Require Fin.
 
 Section Halving.
   Context (T : cmtyp).
@@ -174,8 +167,6 @@ Section EvaluationClosure.
 
 End EvaluationClosure.
 
-Require Fin.
-
 Definition transfer {A} {T : A -> Type} {x y : A} (EQ : x = y) (t : T x) : T y :=
   eq_rect x T t y EQ.
 
diff --git a/lib/ModuRes/MetricCore.v b/lib/ModuRes/MetricCore.v
index 5a4ec2dad..17d989b0b 100644
--- a/lib/ModuRes/MetricCore.v
+++ b/lib/ModuRes/MetricCore.v
@@ -1001,3 +1001,11 @@ Section Option.
 End Option.
 
 Arguments dist {_ _ _} _ _ _ /.
+
+(* We have several users of this, so deifne it centrally *)
+Module NatDec.
+  Definition U := nat.
+  Definition eq_dec := eq_nat_dec.
+End NatDec.
+
+Module D := Coq.Logic.Eqdep_dec.DecidableEqDep(NatDec).
-- 
GitLab