Use : Set explicitly instead of relying on inductive minimization

Instance/Comp.v

@@ -250,7 +250,7 @@ Section Examples.
    and long. *)
 
 (* Group operations *)
-Inductive Group_operation :=
+Inductive Group_operation : Set :=
   | one : Group_operation  (* unit *)
   | mul : Group_operation  (* multiplication *)
   | inv : Group_operation. (* inverse *)
@@ -283,7 +283,7 @@ Definition inv' {G : OpAlgebra GroupOp} (x : G) :=
   op G inv (fun _ => x).
 
 (* There are five group equations. *)
-Inductive Group_equation :=
+Inductive Group_equation : Set :=
   | assoc : Group_equation
   | unit_left : Group_equation
   | unit_right : Group_equation

Instance/Lambda/Eval.v

@@ -17,14 +17,14 @@ Section Eval.
 
 Import ListNotations.
 
-Inductive Closed : Ty → Type :=
+Inductive Closed : Ty → Set :=
   | Closure {Γ τ} : Exp Γ τ → ClEnv Γ → Closed τ
 
-with ClEnv : Env → Type :=
+with ClEnv : Env → Set :=
   | NoCl : ClEnv []
   | AddCl {Γ τ} : Value τ → ClEnv Γ → ClEnv (τ :: Γ)
 
-with Value : Ty → Type :=
+with Value : Ty → Set :=
   | Val {Γ τ} (x : Exp Γ τ) : ValueP x → ClEnv Γ → Value τ.
 
 Derive Signature NoConfusion NoConfusionHom Subterm for ClEnv Closed Value.
@@ -43,7 +43,7 @@ Fixpoint snoc {a : Type} (x : a) (xs : list a) : list a :=
   | x :: xs => x :: snoc x xs
   end.
 
-Inductive EvalContext : Ty → Ty → Type :=
+Inductive EvalContext : Ty → Ty → Set :=
   | MT {τ} : EvalContext τ τ
   | AR {dom cod τ} :
     Closed dom → EvalContext cod τ → EvalContext (dom ⟶ cod) τ
@@ -56,7 +56,7 @@ Inductive EvalContext : Ty → Ty → Type :=
 
 Derive Signature NoConfusion NoConfusionHom Subterm for EvalContext.
 
-Inductive Σ : Ty → Type :=
+Inductive Σ : Ty → Set :=
   | MkΣ {u    : Ty}
         (exp  : Closed u)
         {τ    : Ty}

Instance/Lambda/Exp.v

@@ -19,13 +19,13 @@ Open Scope Ty_scope.
 
 Definition Env := list Ty.
 
-Inductive Var : Env → Ty → Type :=
+Inductive Var : Env → Ty → Set :=
   | ZV {Γ τ}    : Var (τ :: Γ) τ
   | SV {Γ τ τ'} : Var Γ τ → Var (τ' :: Γ) τ.
 
 Derive Signature NoConfusion EqDec for Var.
 
-Inductive Exp Γ : Ty → Type :=
+Inductive Exp Γ : Ty → Set :=
   | EUnit         : Exp Γ TyUnit
 
   | Pair {τ1 τ2}  : Exp Γ τ1 → Exp Γ τ2 → Exp Γ (TyPair τ1 τ2)

Instance/Lambda/Full.v

@@ -24,7 +24,7 @@ Open Scope Ty_scope.
 
 (* A context defines a hole which, after substitution, yields an expression of
    the index type. *)
-Inductive Frame Γ : Ty → Ty → Type :=
+Inductive Frame Γ : Ty → Ty → Set :=
   | F_PairL {τ1 τ2}  : Exp Γ τ2 → Frame τ1 (τ1 × τ2)
   | F_PairR {τ1 τ2}  : Exp Γ τ1 → Frame τ2 (τ1 × τ2)
   | F_Fst {τ1 τ2}    : Frame (τ1 × τ2) τ1
@@ -34,7 +34,7 @@ Inductive Frame Γ : Ty → Ty → Type :=
 
 Derive Signature NoConfusion Subterm for Frame.
 
-Inductive Ctxt Γ : Ty → Ty → Type :=
+Inductive Ctxt Γ : Ty → Ty → Set :=
   | C_Nil {τ}         : Ctxt τ τ
   | C_Cons {τ τ' τ''} : Frame Γ τ' τ → Ctxt τ'' τ' → Ctxt τ'' τ.
 
@@ -65,7 +65,7 @@ Theorem Ctxt_comp_assoc {Γ τ τ' τ'' τ'''}
   Ctxt_comp C (Ctxt_comp C' C'') = Ctxt_comp (Ctxt_comp C C') C''.
 Proof. induction C; simpl; auto; now f_equal. Qed.
 
-Inductive Redex {Γ} : ∀ {τ}, Exp Γ τ → Exp Γ τ → Type :=
+Inductive Redex {Γ} : ∀ {τ}, Exp Γ τ → Exp Γ τ → Set :=
   | R_Beta {dom cod} (e : Exp (dom :: Γ) cod) v :
     ValueP v →
     Redex (APP (LAM e) v) (SubExp {|| v ||} e)
@@ -82,7 +82,7 @@ Derive Signature for Redex.
 
 Unset Elimination Schemes.
 
-Inductive Plug {Γ τ'} (e : Exp Γ τ') : ∀ {τ}, Ctxt Γ τ' τ → Exp Γ τ → Type :=
+Inductive Plug {Γ τ'} (e : Exp Γ τ') : ∀ {τ}, Ctxt Γ τ' τ → Exp Γ τ → Set :=
   | Plug_Hole : Plug (C_Nil _) e
 
   | Plug_PairL {τ1 τ2} {C : Ctxt Γ τ' τ1} {e' : Exp Γ τ1} {e2 : Exp Γ τ2} :
@@ -147,7 +147,7 @@ Theorem Plug_id_left {Γ τ τ'} {C : Ctxt Γ τ' τ} {x : Exp Γ τ'} {y : Exp
   Plug_comp Plug_id P ~= P.
 *)
 
-Inductive Step {Γ τ} : Exp Γ τ → Exp Γ τ → Type :=
+Inductive Step {Γ τ} : Exp Γ τ → Exp Γ τ → Set :=
   | StepRule {τ'} {C : Ctxt Γ τ' τ} {e1 e2 : Exp Γ τ'} {e1' e2' : Exp Γ τ} :
     Plug e1 C e1' →
     Plug e2 C e2' →

Instance/Lambda/Ren.v

@@ -15,7 +15,7 @@ Section Ren.
 
 Import ListNotations.
 
-Inductive Ren : Env → Env → Type :=
+Inductive Ren : Env → Env → Set :=
   | NoRen : Ren [] []
   | Drop {τ Γ Γ'} : Ren Γ Γ' → Ren (τ :: Γ) Γ'
   | Keep {τ Γ Γ'} : Ren Γ Γ' → Ren (τ :: Γ) (τ :: Γ').

Instance/Lambda/Step.v

@@ -25,7 +25,7 @@ Open Scope Ty_scope.
 
 Reserved Notation " t '--->' t' " (at level 40).
 
-Inductive Step : ∀ {Γ τ}, Exp Γ τ → Exp Γ τ → Type :=
+Inductive Step : ∀ {Γ τ}, Exp Γ τ → Exp Γ τ → Set :=
   | ST_Pair1 Γ τ1 τ2 (x x' : Exp Γ τ1) (y : Exp Γ τ2) :
     x ---> x' →
     Pair x y ---> Pair x' y

Instance/Lambda/Sub.v

@@ -16,7 +16,7 @@ Section Sub.
 
 Import ListNotations.
 
-Inductive Sub (Γ : Env) : Env → Type :=
+Inductive Sub (Γ : Env) : Env → Set :=
   | NoSub : Sub []
   | Push {Γ' τ} : Exp Γ τ → Sub Γ' → Sub (τ :: Γ').
 

Instance/Lambda/Ty.v

@@ -7,7 +7,7 @@ Set Transparent Obligations.
 
 Section Ty.
 
-Inductive Ty : Type :=
+Inductive Ty : Set :=
   | TyUnit  : Ty
   | TyPair  : Ty → Ty → Ty
   | TyArrow : Ty → Ty → Ty.

Instance/Lambda/Value.v

@@ -16,7 +16,7 @@ Open Scope Ty_scope.
 
 (* [ValueP] is an inductive proposition that indicates whether an expression
    represents a value, i.e., that it does reduce any further. *)
-Inductive ValueP Γ : ∀ {τ}, Exp Γ τ → Type :=
+Inductive ValueP Γ : ∀ {τ}, Exp Γ τ → Set :=
   | UnitP : ValueP EUnit
   | PairP {τ1 τ2} {x : Exp Γ τ1} {y : Exp Γ τ2} :
     ValueP x → ValueP y → ValueP (Pair x y)

Instance/Parallel.v

@@ -12,9 +12,9 @@ Generalizable All Variables.
 
   This is used to build diagrams that identify equalizers. *)
 
-Inductive ParObj : Type := ParX | ParY.
+Inductive ParObj : Set := ParX | ParY.
 
-Inductive ParHom : bool → ParObj → ParObj → Type :=
+Inductive ParHom : bool → ParObj → ParObj → Set :=
   | ParIdX : ParHom true ParX ParX
   | ParIdY : ParHom true ParY ParY
   | ParOne : ParHom true ParX ParY

Instance/Roof.v

@@ -15,9 +15,9 @@ Generalizable All Variables.
 
   This is used to build diagrams that identify spans and pullbacks. *)
 
-Inductive RoofObj : Type := RNeg | RZero | RPos.
+Inductive RoofObj : Set := RNeg | RZero | RPos.
 
-Inductive RoofHom : RoofObj → RoofObj → Type :=
+Inductive RoofHom : RoofObj → RoofObj → Set :=
   | IdNeg   : RoofHom RNeg  RNeg
   | ZeroNeg : RoofHom RZero RNeg
   | IdZero  : RoofHom RZero RZero

Instance/Shapes.v

@@ -78,7 +78,7 @@ Qed.
 
 (**************************************************************************)
 
-Inductive Shape :=
+Inductive Shape : Set :=
   | Bottom
   | Top
   | Plus (x y : Shape)

Instance/Two.v

@@ -4,9 +4,9 @@ Require Import Category.Theory.Functor.
 
 Generalizable All Variables.
 
-Inductive TwoObj : Type := TwoX | TwoY.
+Inductive TwoObj : Set := TwoX | TwoY.
 
-Inductive TwoHom : TwoObj → TwoObj → Type :=
+Inductive TwoHom : TwoObj → TwoObj → Set :=
   | TwoIdX : TwoHom TwoX TwoX
   | TwoIdY : TwoHom TwoY TwoY
   | TwoXY  : TwoHom TwoX TwoY.

Instance/Two/Discrete.v

@@ -4,9 +4,9 @@ Require Import Category.Theory.Functor.
 
 Generalizable All Variables.
 
-Inductive TwoDObj : Type := TwoDX | TwoDY.
+Inductive TwoDObj : Set := TwoDX | TwoDY.
 
-Inductive TwoDHom : TwoDObj → TwoDObj → Type :=
+Inductive TwoDHom : TwoDObj → TwoDObj → Set :=
   | TwoDIdX : TwoDHom TwoDX TwoDX
   | TwoDIdY : TwoDHom TwoDY TwoDY.
 

Lib/MapDecide.v

@@ -41,11 +41,11 @@ Notation "x && y" := (if x then Reduce y else No) : partial_scope.
  * A term language for theorems involving FMaps
  *)
 
-Record environment := {
+Record environment : Set := {
   vars : positive → N
 }.
 
-Inductive term :=
+Inductive term : Set :=
   | Var   : positive → term
   | Value : N → term.
 
@@ -118,7 +118,7 @@ Fixpoint map_expr_denote env (m : map_expr) : M.t N :=
                           (term_denote env  f) (map_expr_denote env m')
   end.
 
-Inductive formula :=
+Inductive formula : Set :=
   | Top    : formula
   | Bottom : formula
   | Maps   : term → term → term → map_expr → formula

Theory/Metacategory/ArrowsOnly.v

@@ -48,13 +48,13 @@ Section Category.
 
 Context (M : Metacategory).
 
-Record object := {
+Record object : Set := {
   obj_arr : arrow M;
   obj_def : composite M obj_arr obj_arr obj_arr;
   obj_id  : is_identity M obj_arr
 }.
 
-Record morphism (dom cod : object) := {
+Record morphism (dom cod : object) : Set := {
   mor_arr : arrow M;
   mor_dom : composite M mor_arr (obj_arr dom) mor_arr;
   mor_cod : composite M (obj_arr cod) mor_arr mor_arr