compile again

lib/ModuRes/CBUltInst.v

 (** 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.

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.
 

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).