Commit c71c9250 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'avoid-constr-hints' into 'master'

Avoid using Hint Resolve with a term

See merge request iris/iris!390
parents 179725af ba7e4c46
......@@ -11,7 +11,8 @@ Implicit Types Φ : val Λ → iProp Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Hint Resolve head_prim_reducible head_reducible_prim_step : core.
Hint Resolve (reducible_not_val _ inhabitant) : core.
Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
Hint Resolve reducible_not_val_inhabitant : core.
Hint Resolve head_stuck_stuck : core.
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
......
......@@ -209,7 +209,8 @@ Section ectx_lifting.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types e : expr Λ.
Hint Resolve head_prim_reducible head_reducible_prim_step : core.
Hint Resolve (reducible_not_val _ inhabitant) : core.
Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
Hint Resolve reducible_not_val_inhabitant : core.
Hint Resolve head_stuck_stuck : core.
Lemma ownP_lift_head_step s E Φ e1 :
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment