diff --git a/template-coq/theories/AstUtils.v b/template-coq/theories/AstUtils.v
index d3603d0e2..6ebd57b8e 100644
--- a/template-coq/theories/AstUtils.v
+++ b/template-coq/theories/AstUtils.v
@@ -7,6 +7,8 @@ From MetaCoq.Template Require Import Ast.
 Require Import ssreflect ssrbool.
 Require Import ZArith.
 
+#[local] Set Universe Polymorphism.
+
 (** Raw term printing *)
 
 Module string_of_term_tree.
diff --git a/template-coq/theories/Lib.v b/template-coq/theories/Lib.v
index 7a9e95814..0c02486e0 100644
--- a/template-coq/theories/Lib.v
+++ b/template-coq/theories/Lib.v
@@ -91,7 +91,7 @@ Notation tPro x A b :=
 Notation tLet x A t b :=
   (tLetIn {| binder_name := nNamed x; binder_relevance := Relevant |} t A b).
 
-(*Notation "'__'" := (hole) (no associativity, at level 0).*)
+Notation "'__'" := (hole) (no associativity, at level 0).
 
 (** * Monadic notations. *)