more fixes

MetaCoq · Nov 23, 2024 · f50193f · f50193f
1 parent 17fa202
commit f50193f
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/template-coq/theories/Lib.v b/template-coq/theories/Lib.v
@@ -77,8 +77,6 @@ Notation "'$quote_def_rec' x" :=
 Definition term_eqb (t1 t2 : term) :=
   @eq_term config.default_checker_flags init_graph t1 t2.
 
-Notation "t == u" := (term_eqb t u) (at level 70).
-
 (** Short-form notation for [tLambda]. *)
 Notation tLam x A b :=
   (tLambda {| binder_name := nNamed x; binder_relevance := Relevant |} A b).