Commit 7314c3d3 authored by Janno's avatar Janno

Revert "Make heap_lang/proofmode.v universe polymorphic."

This reverts commit b18ebdbd.
parent b18ebdbd
......@@ -6,10 +6,6 @@ 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