Locality can be charged to coq.elpi.add-predicate

LPCIC · Nov 9, 2023 · 2812b72 · 2812b72
1 parent cddb738
commit 2812b72
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi
@@ -69,7 +69,7 @@ pred declare-class-in-coq i:gref.
 declare-class-in-coq ClassGR :- 
   attr->modes CoqModes,
   if (CoqModes = []) true 
-    (@global! => coq.hints.add-mode ClassGR "typeclass_instances" CoqModes),
+    (coq.hints.add-mode ClassGR "typeclass_instances" CoqModes),
   % CAVEAT: this triggers the observer
   coq.TC.declare-class ClassGR,
   attr->search-mode SearchMode,