diff --git a/pcuic/theories/Loader.v b/pcuic/theories/Loader.v
index 0a477ea0c..985ae606a 100644
--- a/pcuic/theories/Loader.v
+++ b/pcuic/theories/Loader.v
@@ -3,5 +3,6 @@ From MetaCoq.Template Require Import Loader.
 From MetaCoq.PCUIC.PCUICTemplateMonad Require Core.
 From MetaCoq.PCUIC Require Import TemplateMonadToPCUIC.
 
-Notation "<% x %>" := (ltac:(let p y := exact y in let p y := run_template_program (@monad_trans Core.TypeInstance Core.TemplateMonad_Monad y) p in quote_term x p))
+(* Work around COQBUG(https://github.com/coq/coq/issues/16715) *)
+Notation "<% x %>" := (match @monad_trans Core.TypeInstance Core.TemplateMonad_Monad return _ with monad_trans => ltac:(let p y := exact y in let p y := run_template_program (monad_trans y) p in quote_term x p) end)
   (only parsing).