tweaks

MetaCoq · Nov 16, 2024 · 0f9d6da · 0f9d6da
1 parent 265e5b6
commit 0f9d6da
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git 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
@@ -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. *)