aboutsummaryrefslogtreecommitdiff
path: root/theories/Program/Combinators.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program/Combinators.v')
-rw-r--r--theories/Program/Combinators.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index 8813131d7b..18e55aefc6 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -40,8 +40,8 @@ Proof.
reflexivity.
Qed.
-Hint Rewrite @compose_id_left @compose_id_right : core.
-Hint Rewrite <- @compose_assoc : core.
+Global Hint Rewrite @compose_id_left @compose_id_right : core.
+Global Hint Rewrite <- @compose_assoc : core.
(** [flip] is involutive. *)