diff --git a/pcuic/theories/TemplateMonadToPCUIC.v b/pcuic/theories/TemplateMonadToPCUIC.v
index fbb0629a6..2799e5ec4 100644
--- a/pcuic/theories/TemplateMonadToPCUIC.v
+++ b/pcuic/theories/TemplateMonadToPCUIC.v
@@ -130,7 +130,7 @@ Section with_tc.
   End with_helper.
 
   Definition monad_trans : (Ast.term -> TemplateMonad term)
-    := tmFix (fun monad_trans => monad_trans' (TransLookup_lookup_inductive' monad_trans)).
+    := tmFix TM (fun monad_trans => monad_trans' (TransLookup_lookup_inductive' monad_trans)).
 
   Definition monad_trans_decl := monad_trans_decl' monad_trans.
   Definition monad_trans_local := monad_trans_local' monad_trans.