Work around coq/coq#16715

MetaCoq · Nov 22, 2022 · f3a8649 · f3a8649
1 parent 0b82c8c
commit f3a8649
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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).