Skip to content
Snippets Groups Projects
Commit c709a9a5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Put global hints in `core`.

parent d5989fe9
Branches
No related tags found
No related merge requests found
Pipeline #21143 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 5 additions and 5 deletions
theories/lang/lifting.v
+ 5
− 5
View file @ c709a9a5
...@@ -29,12 +29,12 @@ Ltac inv_bin_op_eval := ...@@ -29,12 +29,12 @@ Ltac inv_bin_op_eval :=
| H : bin_op_eval _ ?c _ _ _ |- _ => is_constructor c; inversion H; clear H; simplify_eq/= | H : bin_op_eval _ ?c _ _ _ |- _ => is_constructor c; inversion H; clear H; simplify_eq/=
end. end.
Local Hint Extern 0 (atomic _) => solve_atomic. Local Hint Extern 0 (atomic _) => solve_atomic : core.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl. Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Constructors head_step bin_op_eval lit_neq lit_eq. Local Hint Constructors head_step bin_op_eval lit_neq lit_eq : core.
Local Hint Resolve alloc_fresh. Local Hint Resolve alloc_fresh : core.
Local Hint Resolve to_of_val. Local Hint Resolve to_of_val : core.
Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) := Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) :=
as_rec : e = Rec f xl erec. as_rec : e = Rec f xl erec.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment