Commit 7b1face0 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove type argument that was already in the section.

parent 74dfa8b6
......@@ -890,7 +890,7 @@ Proof.
rewrite HQ. destruct p; simpl; auto using wand_elim_r.
Qed.
Class IntoIH {PROP : bi} (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
into_ih : φ of_envs Δ Q.
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
Proof. by rewrite envs_entails_eq /IntoIH. Qed.
......
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