Adapt to coq/coq#17585 (revised warning API)

SkySkimmer · May 22, 2023 · 6aaf7e3 · 6aaf7e3
1 parent eab10de
commit 6aaf7e3
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
@@ -15,11 +15,14 @@ let cast_prop = ref (false)
 
 (* whether Set Template Cast Propositions is on, as needed for erasure in Certicoq *)
 let is_cast_prop () = !cast_prop
+
+let metacoq_cat = CWarnings.create_category ~name:"metacoq" ()
+
 let warn_primitive_turned_into_axiom = 
-  CWarnings.create ~name:"primitive-turned-into-axiom" ~category:"metacoq"
+  CWarnings.create ~name:"primitive-turned-into-axiom" ~category:metacoq_cat
           Pp.(fun prim -> str "Quoting primitive " ++ str prim ++ str " into an axiom.")
 let warn_ignoring_private_polymorphic_universes =
-  CWarnings.create ~name:"private-polymorphic-universes-ignored" ~category:"metacoq"
+  CWarnings.create ~name:"private-polymorphic-universes-ignored" ~category:metacoq_cat
           Pp.(fun () -> str "Ignoring private polymorphic universes.")
 
 let toDecl (old: Name.t Context.binder_annot * ((Constr.constr) option) * Constr.constr) : Constr.rel_declaration =