diff options
| author | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
| commit | 22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (patch) | |
| tree | f4b84d2114aa4523aebf62f020ae46f4321fb10a /theories/Program | |
| parent | ba8e3caa31e464d1007c4ad54e8d70fd70ca3300 (diff) | |
| parent | eeb1d861551e25c6a92721334b3c9f36b7ebb012 (diff) | |
Merge PR #8987: Deprecate hint declaration/removal with no specified database
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Basics.v | 2 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 2 |
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. |