Use : Set explicitly when needed

more robust when using Unset Universe Minimization ToSet cf coq/coq#17810 coq/coq#17795
SkySkimmer · Jul 4, 2023 · 92de04b · 92de04b
1 parent b34d3f3
commit 92de04b
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 8 deletions.
diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v
@@ -10,8 +10,8 @@ Local Set Primitive Projections.
 Local Open Scope bs.
 Import MCMonadNotation.
 
-Class debug_opt := debug : bool.
-Class cls_is_true (b : bool) := is_truev : is_true b.
+Class debug_opt : Set := debug : bool.
+Class cls_is_true (b : bool) : Set := is_truev : is_true b.
 
 (* returns true if a modpath is suitable for quotation, i.e., does not mention functor-bound arguments *)
 Fixpoint modpath_is_absolute (mp : modpath) : bool

diff --git a/quotation/theories/ToPCUIC/Init.v b/quotation/theories/ToPCUIC/Init.v
@@ -16,7 +16,7 @@ Import MCMonadNotation.
 
 Class quotation_of {T} (t : T) := quoted_term_of : PCUICAst.term.
 Class ground_quotable T := quote_ground : forall t : T, quotation_of t.
-Class inductive_quotation_of {T} (t : T)
+Class inductive_quotation_of {T} (t : T) : Set
   := { qinductive : inductive
      ; qinst : Instance.t
      ; qquotation : quotation_of t := tInd qinductive qinst }.
@@ -548,7 +548,7 @@ Definition tmMakeQuotationOfConstantsWorkAroundCoqBug17303 {debug:debug_opt} (in
 Definition tmDeclareQuotationOfConstants {debug:debug_opt} (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (existing_instance : option hint_locality) (base : modpath) (cs : list global_reference) : TemplateMonad unit
   := tmMakeQuotationOfConstants_gen false include_submodule include_supermodule existing_instance base cs (fun name ty _ => @tmAxiom name ty).
 
-Variant submodule_inclusion := only_toplevel | all_submodules_except (_ : list (list ident)) | toplevel_and_submodules (_ : list (list ident)) | everything.
+Variant submodule_inclusion : Set := only_toplevel | all_submodules_except (_ : list (list ident)) | toplevel_and_submodules (_ : list (list ident)) | everything.
 
 #[local] Typeclasses Transparent ident IdentOT.t.
 Definition is_submodule_of (super : list ident) (sub : list ident) : bool

diff --git a/quotation/theories/ToTemplate/Init.v b/quotation/theories/ToTemplate/Init.v
@@ -15,7 +15,7 @@ Import MCMonadNotation.
 
 Class quotation_of {T} (t : T) := quoted_term_of : Ast.term.
 Class ground_quotable T := quote_ground : forall t : T, quotation_of t.
-Class inductive_quotation_of {T} (t : T)
+Class inductive_quotation_of {T} (t : T) : Set
   := { qinductive : inductive
      ; qinst : Instance.t
      ; qquotation : quotation_of t := tInd qinductive qinst }.
@@ -560,7 +560,7 @@ Definition tmMakeQuotationOfConstantsWorkAroundCoqBug17303 {debug:debug_opt} (in
 Definition tmDeclareQuotationOfConstants {debug:debug_opt} (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (existing_instance : option hint_locality) (base : modpath) (cs : list global_reference) : TemplateMonad unit
   := tmMakeQuotationOfConstants_gen false include_submodule include_supermodule existing_instance base cs (fun name ty _ => @tmAxiom name ty).
 
-Variant submodule_inclusion := only_toplevel | all_submodules_except (_ : list (list ident)) | toplevel_and_submodules (_ : list (list ident)) | everything.
+Variant submodule_inclusion : Set := only_toplevel | all_submodules_except (_ : list (list ident)) | toplevel_and_submodules (_ : list (list ident)) | everything.
 
 #[local] Typeclasses Transparent ident IdentOT.t.
 Definition is_submodule_of (super : list ident) (sub : list ident) : bool

diff --git a/template-pcuic/theories/TemplateMonadToPCUIC.v b/template-pcuic/theories/TemplateMonadToPCUIC.v
@@ -169,7 +169,7 @@ End with_tc.
 
 Import TemplateMonad.Core.
 
-Class eval_pcuic_quotation := pcuic_quotation_red_strategy : option reductionStrategy.
+Class eval_pcuic_quotation : Set := pcuic_quotation_red_strategy : option reductionStrategy.
 #[export] Instance default_eval_pcuic_quotation : eval_pcuic_quotation := None.
 
 Definition tmMaybeEval@{t u} `{eval_pcuic_quotation} {A : Type@{t}} (v : A) : TemplateMonad@{t u} A

diff --git a/test-suite/tmFix.v b/test-suite/tmFix.v
@@ -41,7 +41,7 @@ Module TC.
   Local Set Universe Polymorphism.
   Local Unset Universe Minimization ToSet.
   (** This is a kludge, it would be nice to do better *)
-  Class HasFix := tmFix_ : forall {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)), A -> TemplateMonad B.
+  Class HasFix : Prop := tmFix_ : forall {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)), A -> TemplateMonad B.
   (* idk why this is needed... *)
   #[local] Hint Extern 1 (Monad _) => refine TemplateMonad_Monad : typeclass_instances.
   Import MCMonadNotation.