Skip to content
Snippets Groups Projects
Commit f8ef60fe authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make `wp_expr_eval` a `Tactic Notation` so that the argument is parsed as a tactic.

parent df17e4c2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/heap_lang/proofmode.v
+ 1
− 1
View file @ f8ef60fe
...@@ -10,7 +10,7 @@ Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' : ...@@ -10,7 +10,7 @@ Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}). envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
Proof. by intros ->. Qed. Proof. by intros ->. Qed.
Ltac wp_expr_eval t := Tactic Notation "wp_expr_eval" tactic(t) :=
try iStartProof; try iStartProof;
try (eapply tac_wp_expr_eval; [t; reflexivity|]). try (eapply tac_wp_expr_eval; [t; reflexivity|]).
......
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