diff --git a/common/theories/Environment.v b/common/theories/Environment.v
index 07df9efd0..1dc794693 100644
--- a/common/theories/Environment.v
+++ b/common/theories/Environment.v
@@ -242,6 +242,7 @@ Module Environment (T : Term).
     (* Closed type: on well-formed constructors: forall params, cstr_args, I params cstr_indices *)
     cstr_arity : nat; (* arity, w/o lets, w/o parameters *)
   }.
+  Derive NoConfusion EqDec for constructor_body.
 
   Record projection_body := {
     proj_name : ident;
@@ -250,6 +251,7 @@ Module Environment (T : Term).
     proj_relevance : relevance;
     proj_type : term; (* Type under context of params and inductive object *)
   }.
+  Derive NoConfusion EqDec for projection_body.
 
   Definition map_constructor_body npars arities f c :=
     {| cstr_name := c.(cstr_name);
@@ -277,6 +279,7 @@ Module Environment (T : Term).
     ind_ctors : list constructor_body;
     ind_projs : list projection_body; (* names and types of projections, if any. *)
     ind_relevance : relevance (* relevance of the inductive definition *) }.
+  Derive NoConfusion EqDec for one_inductive_body.
 
   Definition map_one_inductive_body npars arities f m :=
     match m with
@@ -296,6 +299,7 @@ Module Environment (T : Term).
     ind_bodies : list one_inductive_body ;
     ind_universes : universes_decl;
     ind_variance : option (list Universes.Variance.t) }.
+  Derive NoConfusion EqDec for mutual_inductive_body.
 
   (** See [constant_body] from [declarations.ml] *)
   Record constant_body := {
@@ -303,6 +307,7 @@ Module Environment (T : Term).
     cst_body : option term;
     cst_universes : universes_decl;
     cst_relevance : relevance }.
+  Derive NoConfusion EqDec for constant_body.
 
   Definition map_constant_body f decl :=
     {| cst_type := f decl.(cst_type);
@@ -321,7 +326,7 @@ Module Environment (T : Term).
   Inductive global_decl :=
   | ConstantDecl : constant_body -> global_decl
   | InductiveDecl : mutual_inductive_body -> global_decl.
-  Derive NoConfusion for global_decl.
+  Derive NoConfusion EqDec for global_decl.
 
   Definition global_declarations := list (kername * global_decl).
 
diff --git a/common/theories/Universes.v b/common/theories/Universes.v
index 3bee4f6d4..0ffe1e67b 100644
--- a/common/theories/Universes.v
+++ b/common/theories/Universes.v
@@ -1774,6 +1774,18 @@ Inductive universes_decl : Type :=
 
 Derive NoConfusion for universes_decl.
 
+Definition universes_decl_eq_dec (x y : universes_decl) : {x = y} + {x <> y}.
+Proof.
+  destruct x as [|x], y as [|y];
+    try solve [ constructor; constructor; constructor
+              | right; abstract congruence ].
+  destruct ((_ : EqDec AUContext.t) x y); [ left | right ].
+  { apply f_equal; assumption. }
+  { abstract congruence. }
+Defined.
+
+#[global] Instance universes_decl_EqDec : EqDec universes_decl := { eq_dec := universes_decl_eq_dec }.
+
 Definition levels_of_udecl u :=
   match u with
   | Monomorphic_ctx => LevelSet.empty