diff options
Diffstat (limited to 'plugins/btauto/Reflect.v')
| -rw-r--r-- | plugins/btauto/Reflect.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index 4cde08872f..98f5ab067a 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -77,10 +77,10 @@ intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto. end. Qed. -Hint Extern 5 => change 0 with (min 0 0). -Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat. -Local Hint Constructors valid. -Hint Extern 5 => zify; omega. +Hint Extern 5 => change 0 with (min 0 0) : core. +Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core. +Local Hint Constructors valid : core. +Hint Extern 5 => zify; omega : core. (* Compatibility with validity *) |