Verified Commit ba7e4c46 authored by Tej Chajed's avatar Tej Chajed

Avoid using Hint Resolve with a term

This feature is now deprecated in Coq master (see
https://github.com/coq/coq/pull/7791).

Instead of passing a partially-applied lemma directly to Hint Resolve,
first create a definition and then make that reference a hint.
parent a2f75cd0
......@@ -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