aboutsummaryrefslogtreecommitdiff
path: root/theories/Program
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program')
-rw-r--r--theories/Program/Basics.v2
-rw-r--r--theories/Program/Wf.v2
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index c2316689fc..d86112abc0 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -26,7 +26,7 @@ Arguments id {A} x.
Definition compose {A B C} (g : B -> C) (f : A -> B) :=
fun x : A => g (f x).
-Hint Unfold compose.
+Hint Unfold compose : core.
Declare Scope program_scope.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 8479b9a2bb..f9d23e3cf6 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -110,7 +110,7 @@ Section Measure_well_founded.
End Measure_well_founded.
-Hint Resolve measure_wf.
+Hint Resolve measure_wf : core.
Section Fix_rects.