From c13ee61fb280b6b33e4bf687fdb27c90ccffaf21 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sun, 7 Aug 2016 12:44:07 +0200 Subject: [PATCH] Remove some useless uses of upred_tactics. --- heap_lang/wp_tactics.v | 1 - proofmode/class_instances.v | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v index ff18e12da..08a4c4c43 100644 --- a/heap_lang/wp_tactics.v +++ b/heap_lang/wp_tactics.v @@ -1,4 +1,3 @@ -From iris.algebra Require Export upred_tactics. From iris.heap_lang Require Export tactics derived. Import uPred. diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v index 3f0fbc015..ff5944225 100644 --- a/proofmode/class_instances.v +++ b/proofmode/class_instances.v @@ -1,5 +1,5 @@ From iris.proofmode Require Export classes. -From iris.algebra Require Import upred_big_op gmap upred_tactics. +From iris.algebra Require Import upred_big_op gmap. Import uPred. Section classes. @@ -225,7 +225,7 @@ Global Instance frame_sep_l R P1 P2 Q Q' : Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed. Global Instance frame_sep_r R P1 P2 Q Q' : Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ★ P2) Q' | 10. -Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed. +Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed. Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ. Global Instance make_and_true_l P : MakeAnd True P P. -- GitLab