diff options
Diffstat (limited to 'common/Separation.v')
| -rw-r--r-- | common/Separation.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Separation.v b/common/Separation.v index 0357b2bf..bf134a18 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -113,7 +113,7 @@ Proof. intros P Q [[A B] [C D]]. split; auto. Qed. -Hint Resolve massert_imp_refl massert_eqv_refl : core. +Global Hint Resolve massert_imp_refl massert_eqv_refl : core. (** * Separating conjunction *) |