Commit b18ebdbd authored by Janno's avatar Janno

Make heap_lang/proofmode.v universe polymorphic.

parent 4145fe5b
......@@ -6,6 +6,10 @@ From Mtac2 Require Import Mtac2 Ttactics DecomposeApp MTeleMatch.
Set Default Proof Using "Type".
Import uPred.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Unset Universe Minimization ToSet.
Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
e = e'
envs_entails Δ (WP e' @ s; E {{ Φ }}) envs_entails Δ (WP e @ s; E {{ Φ }}).
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