Add EqDec instances for various records in the env

Specifically `constructor_body`, `projection_body`,
`one_inductive_body`, `mutual_inductive_body`, `constant_body`,
`global_decl`, `global_decl`, `universes_decl`.

This is needed for Gallina quotation of `declared_constant`, which is
needed for quoting `wf`.

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,13 +299,15 @@ 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 := {
     cst_type : 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).
 

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