diff options
Diffstat (limited to 'theories/Sorting/Sorted.v')
| -rw-r--r-- | theories/Sorting/Sorted.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 8cba461082..206eb606d2 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -137,7 +137,9 @@ Section defs. End defs. +#[global] Hint Constructors HdRel : core. +#[global] Hint Constructors Sorted : core. (* begin hide *) |